per cases ;

suppose A2: F₂() = 0 ; :: thesis:

take <*> F₁() ; :: thesis:
thus ( dom (<*> F₁()) = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
P₁[k,(<*> F₁()) /. k] ) ) by A2; :: thesis:

end;

suppose A3: F₂() <> 0 ; :: thesis:

now :: thesis:

assume A4: Seg F₂() = {} ; :: thesis:

now :: thesis:

per cases ;

case F₂() = 0 ; :: thesis:

hence contradiction by A3; :: thesis:

end;

case F₂() <> 0 ; :: thesis:

hence contradiction by A4; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

then reconsider M = Seg F₂() as non empty set ;
A5: for x being Element of M ex y being Element of F₁() st P₁[x,y]

proof

let x be Element of M; :: thesis:
x in Seg F₂() ;
hence ex y being Element of F₁() st P₁[x,y] by A1; :: thesis:

end;

consider f being Function of M,F₁() such that
A6: for x being Element of M holds P₁[x,f . x] from FUNCT_2:sch 3(A5);
dom f = Seg F₂() by FUNCT_2:def 1;
then reconsider q = f as FinSequence by FINSEQ_1:def 2;

now :: thesis:

let u be object ; :: thesis:
A7: rng q c= F₁() by RELAT_1:def 19;
assume u in rng q ; :: thesis:
hence u in F₁() by A7; :: thesis:

end;

then rng q c= F₁() ;
then reconsider q = q as FinSequence of F₁() by FINSEQ_1:def 4;
take q ; :: thesis:

now :: thesis:

let k be Nat; :: thesis:
assume A8: k in Seg F₂() ; :: thesis:
then k in dom q by FUNCT_2:def 1;
then q . k = q /. k by PARTFUN1:def 6;
hence P₁[k,q /. k] by A6, A8; :: thesis:

end;

hence ( dom q = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
P₁[k,q /. k] ) ) by FUNCT_2:def 1; :: thesis:

end;

end;