per cases ( F2() = 0 or F2() <> 0 ) ;
suppose A2: F2() = 0 ; :: thesis: ex p being FinSequence of F1() st
( dom p = Seg F2() & ( for k being Nat st k in Seg F2() holds
P1[k,p /. k] ) )

take <*> F1() ; :: thesis: ( dom (<*> F1()) = Seg F2() & ( for k being Nat st k in Seg F2() holds
P1[k,(<*> F1()) /. k] ) )

thus ( dom (<*> F1()) = Seg F2() & ( for k being Nat st k in Seg F2() holds
P1[k,(<*> F1()) /. k] ) ) by A2; :: thesis: verum
end;
suppose A3: F2() <> 0 ; :: thesis: ex p being FinSequence of F1() st
( dom p = Seg F2() & ( for k being Nat st k in Seg F2() holds
P1[k,p /. k] ) )

now :: thesis: not Seg F2() = {}
assume A4: Seg F2() = {} ; :: thesis: contradiction
now :: thesis: ( ( F2() = 0 & contradiction ) or ( F2() <> 0 & contradiction ) )end;
hence contradiction ; :: thesis: verum
end;
then reconsider M = Seg F2() as non empty set ;
A5: for x being Element of M ex y being Element of F1() st P1[x,y]
proof
let x be Element of M; :: thesis: ex y being Element of F1() st P1[x,y]
x in Seg F2() ;
hence ex y being Element of F1() st P1[x,y] by A1; :: thesis: verum
end;
consider f being Function of M,F1() such that
A6: for x being Element of M holds P1[x,f . x] from dom f = Seg F2() by FUNCT_2:def 1;
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 F1()
let u be object ; :: thesis: ( u in rng q implies u in F1() )
A7: rng q c= F1() by RELAT_1:def 19;
assume u in rng q ; :: thesis: u in F1()
hence u in F1() by A7; :: thesis: verum
end;
then rng q c= F1() ;
then reconsider q = q as FinSequence of F1() by FINSEQ_1:def 4;
take q ; :: thesis: ( dom q = Seg F2() & ( for k being Nat st k in Seg F2() holds
P1[k,q /. k] ) )

now :: thesis: for k being Nat st k in Seg F2() holds
P1[k,q /. k]
let k be Nat; :: thesis: ( k in Seg F2() implies P1[k,q /. k] )
assume A8: k in Seg F2() ; :: thesis: P1[k,q /. k]
then k in dom q by FUNCT_2:def 1;
then q . k = q /. k by PARTFUN1:def 6;
hence P1[k,q /. k] by A6, A8; :: thesis: verum
end;
hence ( dom q = Seg F2() & ( for k being Nat st k in Seg F2() holds
P1[k,q /. k] ) ) by FUNCT_2:def 1; :: thesis: verum
end;
end;