let F, G be Function of (product <*G1,G2*>),(product <*H1,H2*>); ( ( 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)*> )
; F = G
now for x being Element of (product <*G1,G2*>) holds F . x = G . xlet x be
Element of
(product <*G1,G2*>);
F . x = G . xconsider 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;
verum end;
hence
F = G
; verum