defpred S_{1}[ object , object ] means for x1, y1, w1 being object st $1 = [x1,y1,w1] holds

P_{1}[x1,y1,w1,$2];

A2: for x being object st x in [:F_{1}(),F_{2}(),F_{3}():] holds

ex z being object st

( z in F_{4}() & S_{1}[x,z] )
_{1}(),F_{2}(),F_{3}():],F_{4}() such that

A8: for x being object st x in [:F_{1}(),F_{2}(),F_{3}():] holds

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

take f ; :: thesis: for x, y, w being object st x in F_{1}() & y in F_{2}() & w in F_{3}() holds

P_{1}[x,y,w,f . (x,y,w)]

thus for x, y, w being object st x in F_{1}() & y in F_{2}() & w in F_{3}() holds

P_{1}[x,y,w,f . (x,y,w)]
by A8, MCART_1:69; :: thesis: verum

P

A2: for x being object st x in [:F

ex z being object st

( z in F

proof

consider f being Function of [:F
let x be object ; :: thesis: ( x in [:F_{1}(),F_{2}(),F_{3}():] implies ex z being object st

( z in F_{4}() & S_{1}[x,z] ) )

assume x in [:F_{1}(),F_{2}(),F_{3}():]
; :: thesis: ex z being object st

( z in F_{4}() & S_{1}[x,z] )

then consider x1, y1, w1 being object such that

A3: ( x1 in F_{1}() & y1 in F_{2}() & w1 in F_{3}() )
and

A4: x = [x1,y1,w1] by MCART_1:68;

consider z being object such that

A5: z in F_{4}()
and

A6: P_{1}[x1,y1,w1,z]
by A1, A3;

take z ; :: thesis: ( z in F_{4}() & S_{1}[x,z] )

thus z in F_{4}()
by A5; :: thesis: S_{1}[x,z]

let x2, y2, w2 be object ; :: thesis: ( x = [x2,y2,w2] implies P_{1}[x2,y2,w2,z] )

assume A7a: x = [x2,y2,w2] ; :: thesis: P_{1}[x2,y2,w2,z]

then ( [x1,y1] = [x2,y2] & w1 = w2 ) by A4, XTUPLE_0:1;

then ( x1 = x2 & y1 = y2 ) by XTUPLE_0:1;

hence P_{1}[x2,y2,w2,z]
by A6, A7a, A4, XTUPLE_0:1; :: thesis: verum

end;( z in F

assume x in [:F

( z in F

then consider x1, y1, w1 being object such that

A3: ( x1 in F

A4: x = [x1,y1,w1] by MCART_1:68;

consider z being object such that

A5: z in F

A6: P

take z ; :: thesis: ( z in F

thus z in F

let x2, y2, w2 be object ; :: thesis: ( x = [x2,y2,w2] implies P

assume A7a: x = [x2,y2,w2] ; :: thesis: P

then ( [x1,y1] = [x2,y2] & w1 = w2 ) by A4, XTUPLE_0:1;

then ( x1 = x2 & y1 = y2 ) by XTUPLE_0:1;

hence P

A8: for x being object st x in [:F

S

take f ; :: thesis: for x, y, w being object st x in F

P

thus for x, y, w being object st x in F

P