let X1, X2 be set ; :: thesis: ( ex L being Sequence st
( X1 = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L & d1 in union {(L . B)} ) } & dom L = A & ( for B being Ordinal st B in A holds
L . B = { d1 where d1 is Element of E : for d being Element of E st d in d1 holds
ex C being Ordinal st
( C in dom (L | B) & d in union {((L | B) . C)} ) } ) ) & ex L being Sequence st
( X2 = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L & d1 in union {(L . B)} ) } & dom L = A & ( for B being Ordinal st B in A holds
L . B = { d1 where d1 is Element of E : for d being Element of E st d in d1 holds
ex C being Ordinal st
( C in dom (L | B) & d in union {((L | B) . C)} ) } ) ) implies X1 = X2 )
given L being Sequence such that A3: ( X1 = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L & d1 in union {(L . B)} ) } & dom L = A & ( for B being Ordinal st B in A holds
L . B = { d1 where d1 is Element of E : for d being Element of E st d in d1 holds
ex C being Ordinal st
( C in dom (L | B) & d in union {((L | B) . C)} ) } ) ) ; :: thesis: ( for L being Sequence holds
( not X2 = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L & d1 in union {(L . B)} ) } or not dom L = A or ex B being Ordinal st
( B in A & not L . B = { d1 where d1 is Element of E : for d being Element of E st d in d1 holds
ex C being Ordinal st
( C in dom (L | B) & d in union {((L | B) . C)} ) } ) ) or X1 = X2 )
A4: ( dom L = A & ( for B being Ordinal
for L1 being Sequence st B in A & L1 = L | B holds
L . B = H₁(L1) ) ) by A3;
given L1 being Sequence such that A5: ( X2 = { d where d is Element of E : for d1 being Element of E st d1 in d holds
ex B being Ordinal st
( B in dom L1 & d1 in union {(L1 . B)} ) } & dom L1 = A & ( for B being Ordinal st B in A holds
L1 . B = { d1 where d1 is Element of E : for d being Element of E st d in d1 holds
ex C being Ordinal st
( C in dom (L1 | B) & d in union {((L1 | B) . C)} ) } ) ) ; :: thesis: X1 = X2
A6: ( dom L1 = A & ( for B being Ordinal
for L being Sequence st B in A & L = L1 | B holds
L1 . B = H₁(L) ) ) by A5;
L = L1 from ORDINAL1:sch 3(A4, A6);
hence X1 = X2 by A3, A5; :: thesis: verum