let G, F be non empty addLoopStr ; :: thesis: ex ADGF being Function of [:[: the carrier of G, the carrier of F:],[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for g1, g2 being Point of G
for f1, f2 being Point of F holds ADGF . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
defpred S₁[ set , set , set ] means ex g1, g2 being Point of G ex f1, f2 being Point of F st
( $1 = [g1,f1] & $2 = [g2,f2] & $3 = [(g1 + g2),(f1 + f2)] );
P1: for x, y being set st x in [: the carrier of G, the carrier of F:] & y in [: the carrier of G, the carrier of F:] holds
ex z being set st
( z in [: the carrier of G, the carrier of F:] & S₁[x,y,z] )

proof

let x, y be set ; :: thesis: ( x in [: the carrier of G, the carrier of F:] & y in [: the carrier of G, the carrier of F:] implies ex z being set st
( z in [: the carrier of G, the carrier of F:] & S₁[x,y,z] ) )
assume AS1: ( x in [: the carrier of G, the carrier of F:] & y in [: the carrier of G, the carrier of F:] ) ; :: thesis: ex z being set st
( z in [: the carrier of G, the carrier of F:] & S₁[x,y,z] )
then consider x1 being Point of G, x2 being Point of F such that
P1: x = [x1,x2] by LM01;
consider y1 being Point of G, y2 being Point of F such that
P2: y = [y1,y2] by LM01, AS1;
reconsider z = [(x1 + y1),(x2 + y2)] as Element of [: the carrier of G, the carrier of F:] ;
( z in [: the carrier of G, the carrier of F:] & S₁[x,y,z] ) by P1, P2;
hence ex z being set st
( z in [: the carrier of G, the carrier of F:] & S₁[x,y,z] ) ; :: thesis: verum

end;

consider ADGF being Function of [:[: the carrier of G, the carrier of F:],[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] such that
P2: for x, y being set st x in [: the carrier of G, the carrier of F:] & y in [: the carrier of G, the carrier of F:] holds
S₁[x,y,ADGF . (x,y)] from BINOP_1:sch 1(P1);

now

let g1, g2 be Point of G; :: thesis: for f1, f2 being Point of F holds ADGF . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
let f1, f2 be Point of F; :: thesis: ADGF . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)]
consider gg1, gg2 being Point of G, ff1, ff2 being Point of F such that
P5: ( [g1,f1] = [gg1,ff1] & [g2,f2] = [gg2,ff2] & ADGF . ([g1,f1],[g2,f2]) = [(gg1 + gg2),(ff1 + ff2)] ) by P2;
( g1 = gg1 & f1 = ff1 & g2 = gg2 & f2 = ff2 ) by ZFMISC_1:33, P5;
hence ADGF . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] by P5; :: thesis: verum

end;

hence ex ADGF being Function of [:[: the carrier of G, the carrier of F:],[: the carrier of G, the carrier of F:]:],[: the carrier of G, the carrier of F:] st
for g1, g2 being Point of G
for f1, f2 being Point of F holds ADGF . ([g1,f1],[g2,f2]) = [(g1 + g2),(f1 + f2)] ; :: thesis: verum