deffunc H₁( set ) -> Element of F₁() = F₂((IFXFinSequence ($1,F₁())));
reconsider f1 = F₃() as Function ;
reconsider f2 = F₄() as Function ;
A3: ( dom f1 = NAT & ( for n being Nat holds f1 . n = H₁(f1 | n) ) )

proof

thus dom f1 = NAT by FUNCT_2:def 1; :: thesis: for n being Nat holds f1 . n = H₁(f1 | n)
let n be Nat; :: thesis: f1 . n = H₁(f1 | n)
thus f1 . n = F₂((F₃() | n)) by A1
.= H₁(f1 | n) by Def1 ; :: thesis: verum

end;

A4: ( dom f2 = NAT & ( for n being Nat holds f2 . n = H₁(f2 | n) ) )

proof

thus dom f2 = NAT by FUNCT_2:def 1; :: thesis: for n being Nat holds f2 . n = H₁(f2 | n)
let n be Nat; :: thesis: f2 . n = H₁(f2 | n)
thus f2 . n = F₂((F₄() | n)) by A2
.= H₁(f2 | n) by Def1 ; :: thesis: verum

end;

f1 = f2 from ALGSTR_4:sch 1(A3, A4);
hence F₃() = F₄() ; :: thesis: verum