deffunc H₁( object ) -> set = F₂((sup (union {$1})));
consider f being Function such that
A1: ( dom f = F₁() & ( for x being object st x in F₁() holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
reconsider f = f as Sequence by A1, ORDINAL1:def 7;
take L = f; :: thesis: ( dom L = F₁() & ( for A being Ordinal st A in F₁() holds
L . A = F₂(A) ) )
thus dom L = F₁() by A1; :: thesis: for A being Ordinal st A in F₁() holds
L . A = F₂(A)
let A be Ordinal; :: thesis: ( A in F₁() implies L . A = F₂(A) )
assume A in F₁() ; :: thesis: L . A = F₂(A)
hence L . A = F₂((sup (union {A}))) by A1
.= F₂((sup A)) by ZFMISC_1:25
.= F₂(A) by Th18 ;
:: thesis: verum