A2:
for k being object st k in F_{2}() holds

ex x being object st

( x in F_{1}() & P_{1}[k,x] )
_{2}(),F_{1}() such that

A4: for x being object st x in F_{2}() holds

P_{1}[x,f . x]
from FUNCT_2:sch 1(A2);

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

then reconsider p = f as XFinSequence of F_{1}() by AFINSQ_1:5;

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

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

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

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

ex x being object st

( x in F

proof

consider f being Function of F
let k be object ; :: thesis: ( k in F_{2}() implies ex x being object st

( x in F_{1}() & P_{1}[k,x] ) )

assume A3: k in F_{2}()
; :: thesis: ex x being object st

( x in F_{1}() & P_{1}[k,x] )

F_{2}() is Subset of NAT
by Th8;

then reconsider k9 = k as Element of NAT by A3;

ex x being Element of F_{1}() st P_{1}[k9,x]
by A1, A3;

hence ex x being object st

( x in F_{1}() & P_{1}[k,x] )
; :: thesis: verum

end;( x in F

assume A3: k in F

( x in F

F

then reconsider k9 = k as Element of NAT by A3;

ex x being Element of F

hence ex x being object st

( x in F

A4: for x being object st x in F

P

dom f = F

then reconsider p = f as XFinSequence of F

take p ; :: thesis: ( dom p = Segm F

P

thus ( dom p = Segm F

P