defpred S_{1}[ set ] means $1 in dom fi;

deffunc H_{1}( Ordinal) -> set = psi . ($1 -^ (dom fi));

deffunc H_{2}( 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_{1}[x] implies f . x = H_{2}(x) ) & ( not S_{1}[x] implies f . x = H_{1}(x) ) )
from FINSET_1:sch 1();

reconsider f = f as 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

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

deffunc H

deffunc H

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

reconsider f = f as 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

let A be Ordinal; :: thesis: ( A in dom psi implies f . ((dom fi) +^ A) = psi . A )
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 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

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