defpred S_{1}[ object , object ] means ( P_{1}[$2,$1] & ( for i9 being Element of F_{1}() st $1 = i9 holds

$2 in the carrier of (F_{2}() . i9) ) );

A2: for i being object st i in F_{1}() holds

ex x being object st S_{1}[i,x]

A4: dom f = F_{1}()
and

A5: for i being object st i in F_{1}() holds

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

A6: for x being object st x in dom (Carrier F_{2}()) holds

f . x in (Carrier F_{2}()) . x
_{2}())
by A4, PARTFUN1:def 2;

then f in product (Carrier F_{2}())
by A6, CARD_3:9;

then reconsider f = f as Element of (product F_{2}()) by WAYBEL18:def 3;

take f ; :: thesis: for i being Element of F_{1}() holds P_{1}[f . i,i]

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

thus P_{1}[f . i,i]
by A5; :: thesis: verum

$2 in the carrier of (F

A2: for i being object st i in F

ex x being object st S

proof

consider f being Function such that
let i be object ; :: thesis: ( i in F_{1}() implies ex x being object st S_{1}[i,x] )

assume i in F_{1}()
; :: thesis: ex x being object st S_{1}[i,x]

then reconsider i1 = i as Element of F_{1}() ;

consider x being Element of (F_{2}() . i1) such that

A3: P_{1}[x,i1]
by A1;

take x ; :: thesis: S_{1}[i,x]

thus P_{1}[x,i]
by A3; :: thesis: for i9 being Element of F_{1}() st i = i9 holds

x in the carrier of (F_{2}() . i9)

let i9 be Element of F_{1}(); :: thesis: ( i = i9 implies x in the carrier of (F_{2}() . i9) )

assume i = i9 ; :: thesis: x in the carrier of (F_{2}() . i9)

hence x in the carrier of (F_{2}() . i9)
; :: thesis: verum

end;assume i in F

then reconsider i1 = i as Element of F

consider x being Element of (F

A3: P

take x ; :: thesis: S

thus P

x in the carrier of (F

let i9 be Element of F

assume i = i9 ; :: thesis: x in the carrier of (F

hence x in the carrier of (F

A4: dom f = F

A5: for i being object st i in F

S

A6: for x being object st x in dom (Carrier F

f . x in (Carrier F

proof

dom f = dom (Carrier F
let x be object ; :: thesis: ( x in dom (Carrier F_{2}()) implies f . x in (Carrier F_{2}()) . x )

assume x in dom (Carrier F_{2}())
; :: thesis: f . x in (Carrier F_{2}()) . x

then reconsider x9 = x as Element of F_{1}() ;

f . x9 in the carrier of (F_{2}() . x9)
by A5;

hence f . x in (Carrier F_{2}()) . x
by YELLOW_6:2; :: thesis: verum

end;assume x in dom (Carrier F

then reconsider x9 = x as Element of F

f . x9 in the carrier of (F

hence f . x in (Carrier F

then f in product (Carrier F

then reconsider f = f as Element of (product F

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

let i be Element of F

thus P