deffunc H₁( Sequence) -> set = bool (union (rng $1));
deffunc H₂( Sequence) -> set = [:H₁($1),H₁($1):];
consider L being Sequence such that
A1: dom L = succ A and
A2: for B being Ordinal
for L1 being Sequence st B in succ A & L1 = L | B holds
L . B = H₂(L1) from ORDINAL1:sch 4();
thus ex IT being set ex L being Sequence st
( IT = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:H₁(L | O),H₁(L | O):] ) ) :: thesis: for b₁, b₂ being set st ex L being Sequence st
( b₁ = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) ) & ex L being Sequence st
( b₂ = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) ) holds
b₁ = b₂

proof

take IT = L . A; :: thesis: ex L being Sequence st
( IT = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:H₁(L | O),H₁(L | O):] ) )
take L ; :: thesis: ( IT = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:H₁(L | O),H₁(L | O):] ) )
thus ( IT = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:H₁(L | O),H₁(L | O):] ) ) by A1, A2; :: thesis: verum

end;

let it1, it2 be set ; :: thesis: ( ex L being Sequence st
( it1 = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) ) & ex L being Sequence st
( it2 = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) ) implies it1 = it2 )
given L1 being Sequence such that A3: ( it1 = L1 . A & dom L1 = succ A & ( for O being Ordinal st O in succ A holds
L1 . O = [:H₁(L1 | O),H₁(L1 | O):] ) ) ; :: thesis: ( for L being Sequence holds
( not it2 = L . A or not dom L = succ A or ex O being Ordinal st
( O in succ A & not L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) ) or it1 = it2 )
given L2 being Sequence such that A4: ( it2 = L2 . A & dom L2 = succ A & ( for O being Ordinal st O in succ A holds
L2 . O = [:H₁(L2 | O),H₁(L2 | O):] ) ) ; :: thesis: it1 = it2
A5: ( dom L1 = succ A & ( for B being Ordinal
for L being Sequence st B in succ A & L = L1 | B holds
L1 . B = H₂(L) ) ) by A3;
A6: ( dom L2 = succ A & ( for B being Ordinal
for L being Sequence st B in succ A & L = L2 | B holds
L2 . B = H₂(L) ) ) by A4;
L1 = L2 from ORDINAL1:sch 3(A5, A6);
hence it1 = it2 by A3, A4; :: thesis: verum