defpred S1[ Element of X, Element of product F, Element of product F] means for i being Element of dom F holds $3 . i = (p . i) . ($1,($2 . i));
A1: for x being Element of X
for d being Element of product F ex z being Element of product F st S1[x,d,z]
proof
let x be Element of X; :: thesis: for d being Element of product F ex z being Element of product F st S1[x,d,z]
let d be Element of product F; :: thesis: ex z being Element of product F st S1[x,d,z]
defpred S2[ object , object ] means ex i being Element of dom F st
( $1 = i & $2 = (p . i) . (x,(d . i)) );
A2: for w being object st w in dom F holds
ex z being object st S2[w,z]
proof
let w be object ; :: thesis: ( w in dom F implies ex z being object st S2[w,z] )
assume w in dom F ; :: thesis: ex z being object st S2[w,z]
then reconsider i = w as Element of dom F ;
take (p . i) . (x,(d . i)) ; :: thesis: S2[w,(p . i) . (x,(d . i))]
thus S2[w,(p . i) . (x,(d . i))] ; :: thesis: verum
end;
consider z being Function such that
A3: ( dom z = dom F & ( for w being object st w in dom F holds
S2[w,z . w] ) ) from CLASSES1:sch 1(A2);
now :: thesis: for w being object st w in dom F holds
z . w in F . w
let w be object ; :: thesis: ( w in dom F implies z . w in F . w )
assume w in dom F ; :: thesis: z . w in F . w
then ex i being Element of dom F st
( w = i & z . w = (p . i) . (x,(d . i)) ) by A3;
hence z . w in F . w ; :: thesis: verum
end;
then reconsider z9 = z as Element of product F by A3, CARD_3:9;
take z9 ; :: thesis: S1[x,d,z9]
let i be Element of dom F; :: thesis: z9 . i = (p . i) . (x,(d . i))
ex j being Element of dom F st
( j = i & z . i = (p . j) . (x,(d . j)) ) by A3;
hence z9 . i = (p . i) . (x,(d . i)) ; :: thesis: verum
end;
thus ex P being Function of [:X,(product F):],(product F) st
for x being Element of X
for d being Element of product F holds S1[x,d,P . (x,d)] from BINOP_1:sch 3(A1); :: thesis: verum