let f, h be Element of product (carr G); :: thesis: ( ( for j being Element of dom (carr G) holds f . j = the ZeroF of (G . j) ) & ( for j being Element of dom (carr G) holds h . j = the ZeroF of (G . j) ) implies f = h )
assume that
A17: for j being Element of dom (carr G) holds f . j = the ZeroF of (G . j) and
A18: for j being Element of dom (carr G) holds h . j = the ZeroF of (G . j) ; :: thesis: f = h
reconsider f9 = f, h9 = h as Function ;

A19: now

let x be set ; :: thesis: ( x in dom (carr G) implies f9 . x = h9 . x )
assume x in dom (carr G) ; :: thesis: f9 . x = h9 . x
then reconsider i = x as Element of dom (carr G) ;
thus f9 . x = the ZeroF of (G . i) by A17
.= h9 . x by A18 ; :: thesis: verum

end;

( dom f9 = dom (carr G) & dom h9 = dom (carr G) ) by CARD_3:9;
hence f = h by A19, FUNCT_1:2; :: thesis: verum