defpred S₁[ set ] means $1 in dom fi;
deffunc H₁( Ordinal) -> set = psi . ($1 -^ (dom fi));
deffunc H₂( set ) -> set = fi . $1;
consider f being Function such that
A1: dom f = (dom fi) +^ (dom psi) and
A2: for x being Ordinal st x in (dom fi) +^ (dom psi) holds
( ( S₁[x] implies f . x = H₂(x) ) & ( not S₁[x] implies f . x = H₁(x) ) ) from FINSET_1:sch 1();
reconsider f = f as T-Sequence by A1, ORDINAL1:def 7;
take f ; :: thesis: ( dom f = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
f . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
f . ((dom fi) +^ A) = psi . A ) )
thus dom f = (dom fi) +^ (dom psi) by A1; :: thesis: ( ( for A being Ordinal st A in dom fi holds
f . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
f . ((dom fi) +^ A) = psi . A ) )
thus for A being Ordinal st A in dom fi holds
f . A = fi . A :: thesis: for A being Ordinal st A in dom psi holds
f . ((dom fi) +^ A) = psi . A

proof

A3: dom fi c= dom f by A1, ORDINAL3:24;
let A be Ordinal; :: thesis: ( A in dom fi implies f . A = fi . A )
assume A in dom fi ; :: thesis: f . A = fi . A
hence f . A = fi . A by A1, A2, A3; :: thesis: verum

end;

let A be Ordinal; :: thesis: ( A in dom psi implies f . ((dom fi) +^ A) = psi . A )
dom fi c= (dom fi) +^ A by ORDINAL3:24;
then A4: not (dom fi) +^ A in dom fi by ORDINAL1:5;
assume A in dom psi ; :: thesis: f . ((dom fi) +^ A) = psi . A
then (dom fi) +^ A in dom f by A1, ORDINAL2:32;
then f . ((dom fi) +^ A) = psi . (((dom fi) +^ A) -^ (dom fi)) by A1, A2, A4;
hence f . ((dom fi) +^ A) = psi . A by ORDINAL3:52; :: thesis: verum