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 :: thesis: for x being Element of (product <*G1,G2*>) holds F . x = G . x
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 by A5, A7, FINSEQ_1:77;
hence F . x = G . x by A5, A6, A7, A8, FINSEQ_1:77; :: thesis: verum
end;
hence F = G ; :: thesis: verum