let F, G be Function of (product <*G1,G2*>),(product <*H1,H2*>); :: thesis: ( ( for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> & F . x = <*(f . x1),(g . x2)*> ) ) & ( for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> & G . x = <*(f . x1),(g . x2)*> ) ) implies F = G )
assume that
A3: for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> & F . x = <*(f . x1),(g . x2)*> ) and
A4: for x being Element of (product <*G1,G2*>) ex x1 being Element of G1 ex x2 being Element of G2 st
( x = <*x1,x2*> & G . x = <*(f . x1),(g . x2)*> ) ; :: thesis: F = G

now

let x be Element of (product <*G1,G2*>); :: thesis: F . x = G . x
consider x1 being Element of G1, x2 being Element of G2 such that
A5: x = <*x1,x2*> and
A6: F . x = <*(f . x1),(g . x2)*> by A3;
consider y1 being Element of G1, y2 being Element of G2 such that
A7: x = <*y1,y2*> and
A8: G . x = <*(f . y1),(g . y2)*> by A4;
( x1 = y1 & x2 = y2 ) by A5, A7, GROUP_7:2;
hence F . x = G . x by A6, A8; :: thesis: verum

end;

hence F = G by FUNCT_2:113; :: thesis: verum