consider L being Sequence such that
A1: dom L = A and
A2: for B being Ordinal
for L1 being Sequence st B in A & L1 = L | B holds
L . B = H₁(L1) from ORDINAL1:sch 4();
take x = { 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)} ) } ; :: thesis: ex L being Sequence st
( x = { 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)} ) } ) )
take L ; :: thesis: ( x = { 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)} ) } ) )
thus x = { 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)} ) } ; :: thesis: ( 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)} ) } ) )
thus dom L = A by A1; :: thesis: 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)} ) }
let B be Ordinal; :: thesis: ( B in A implies 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)} ) } )
assume B in A ; :: thesis: 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)} ) }
hence 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)} ) } by A2; :: thesis: verum