per cases
( F_{2}() = 0 or F_{2}() <> 0 )
;

end;

suppose A2:
F_{2}() = 0
; :: thesis: ex p being FinSequence of F_{1}() st

( dom p = Seg F_{2}() & ( for k being Nat st k in Seg F_{2}() holds

P_{1}[k,p /. k] ) )

( dom p = Seg F

P

take
<*> F_{1}()
; :: thesis: ( dom (<*> F_{1}()) = Seg F_{2}() & ( for k being Nat st k in Seg F_{2}() holds

P_{1}[k,(<*> F_{1}()) /. k] ) )

thus ( dom (<*> F_{1}()) = Seg F_{2}() & ( for k being Nat st k in Seg F_{2}() holds

P_{1}[k,(<*> F_{1}()) /. k] ) )
by A2; :: thesis: verum

end;P

thus ( dom (<*> F

P

suppose A3:
F_{2}() <> 0
; :: thesis: ex p being FinSequence of F_{1}() st

( dom p = Seg F_{2}() & ( for k being Nat st k in Seg F_{2}() holds

P_{1}[k,p /. k] ) )

_{2}() as non empty set ;

A5: for x being Element of M ex y being Element of F_{1}() st P_{1}[x,y]
_{1}() such that

A6: for x being Element of M holds P_{1}[x,f . x]
from FUNCT_2:sch 3(A5);

dom f = Seg F_{2}()
by FUNCT_2:def 1;

then reconsider q = f as FinSequence by FINSEQ_1:def 2;

_{1}()
;

then reconsider q = q as FinSequence of F_{1}() by FINSEQ_1:def 4;

take q ; :: thesis: ( dom q = Seg F_{2}() & ( for k being Nat st k in Seg F_{2}() holds

P_{1}[k,q /. k] ) )

_{2}() & ( for k being Nat st k in Seg F_{2}() holds

P_{1}[k,q /. k] ) )
by FUNCT_2:def 1; :: thesis: verum

end;

( dom p = Seg F

P

now :: thesis: not Seg F_{2}() = {}

then reconsider M = Seg Fassume A4:
Seg F_{2}() = {}
; :: thesis: contradiction

end;now :: thesis: ( ( F_{2}() = 0 & contradiction ) or ( F_{2}() <> 0 & contradiction ) )end;

hence
contradiction
; :: thesis: verumA5: for x being Element of M ex y being Element of F

proof

consider f being Function of M,F
let x be Element of M; :: thesis: ex y being Element of F_{1}() st P_{1}[x,y]

x in Seg F_{2}()
;

hence ex y being Element of F_{1}() st P_{1}[x,y]
by A1; :: thesis: verum

end;x in Seg F

hence ex y being Element of F

A6: for x being Element of M holds P

dom f = Seg F

then reconsider q = f as FinSequence by FINSEQ_1:def 2;

now :: thesis: for u being object st u in rng q holds

u in F_{1}()

then
rng q c= Fu in F

let u be object ; :: thesis: ( u in rng q implies u in F_{1}() )

A7: rng q c= F_{1}()
by RELAT_1:def 19;

assume u in rng q ; :: thesis: u in F_{1}()

hence u in F_{1}()
by A7; :: thesis: verum

end;A7: rng q c= F

assume u in rng q ; :: thesis: u in F

hence u in F

then reconsider q = q as FinSequence of F

take q ; :: thesis: ( dom q = Seg F

P

now :: thesis: for k being Nat st k in Seg F_{2}() holds

P_{1}[k,q /. k]

hence
( dom q = Seg FP

let k be Nat; :: thesis: ( k in Seg F_{2}() implies P_{1}[k,q /. k] )

assume A8: k in Seg F_{2}()
; :: thesis: P_{1}[k,q /. k]

then k in dom q by FUNCT_2:def 1;

then q . k = q /. k by PARTFUN1:def 6;

hence P_{1}[k,q /. k]
by A6, A8; :: thesis: verum

end;assume A8: k in Seg F

then k in dom q by FUNCT_2:def 1;

then q . k = q /. k by PARTFUN1:def 6;

hence P

P