defpred S_{1}[ set , set ] means for x being Element of F_{1}()

for y being Element of F_{2}() st $1 = [x,y] holds

P_{1}[x,y,$2];

A2: for p being Element of [:F_{1}(),F_{2}():] ex z being Element of F_{3}() st S_{1}[p,z]
_{1}(),F_{2}():],F_{3}() such that

A8: for p being Element of [:F_{1}(),F_{2}():] holds S_{1}[p,f . p]
from FUNCT_2:sch 3(A2);

take f ; :: thesis: for x being Element of F_{1}()

for y being Element of F_{2}() holds P_{1}[x,y,f . (x,y)]

let x be Element of F_{1}(); :: thesis: for y being Element of F_{2}() holds P_{1}[x,y,f . (x,y)]

let y be Element of F_{2}(); :: thesis: P_{1}[x,y,f . (x,y)]

reconsider xy = [x,y] as Element of [:F_{1}(),F_{2}():] by ZFMISC_1:def 2;

P_{1}[x,y,f . xy]
by A8;

hence P_{1}[x,y,f . (x,y)]
; :: thesis: verum

for y being Element of F

P

A2: for p being Element of [:F

proof

consider f being Function of [:F
let p be Element of [:F_{1}(),F_{2}():]; :: thesis: ex z being Element of F_{3}() st S_{1}[p,z]

consider x1, y1 being object such that

A3: x1 in F_{1}()
and

A4: y1 in F_{2}()
and

A5: p = [x1,y1] by ZFMISC_1:def 2;

reconsider y1 = y1 as Element of F_{2}() by A4;

reconsider x1 = x1 as Element of F_{1}() by A3;

consider z being Element of F_{3}() such that

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

take z ; :: thesis: S_{1}[p,z]

let x be Element of F_{1}(); :: thesis: for y being Element of F_{2}() st p = [x,y] holds

P_{1}[x,y,z]

let y be Element of F_{2}(); :: thesis: ( p = [x,y] implies P_{1}[x,y,z] )

assume A7: p = [x,y] ; :: thesis: P_{1}[x,y,z]

then x1 = x by A5, XTUPLE_0:1;

hence P_{1}[x,y,z]
by A5, A6, A7, XTUPLE_0:1; :: thesis: verum

end;consider x1, y1 being object such that

A3: x1 in F

A4: y1 in F

A5: p = [x1,y1] by ZFMISC_1:def 2;

reconsider y1 = y1 as Element of F

reconsider x1 = x1 as Element of F

consider z being Element of F

A6: P

take z ; :: thesis: S

let x be Element of F

P

let y be Element of F

assume A7: p = [x,y] ; :: thesis: P

then x1 = x by A5, XTUPLE_0:1;

hence P

A8: for p being Element of [:F

take f ; :: thesis: for x being Element of F

for y being Element of F

let x be Element of F

let y be Element of F

reconsider xy = [x,y] as Element of [:F

P

hence P