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

now

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

end;

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