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
A11: for j being Element of dom (carr G) holds f . j = the ZeroF of (G . j) and
A12: for j being Element of dom (carr G) holds h . j = the ZeroF of (G . j) ; :: thesis: f = h
reconsider f' = f, h' = h as Function ;
A13: ( dom f' = dom (carr G) & dom h' = dom (carr G) ) by CARD_3:18;

now

let x be set ; :: thesis: ( x in dom (carr G) implies f' . x = h' . x )
assume x in dom (carr G) ; :: thesis: f' . x = h' . x
then reconsider i = x as Element of dom (carr G) ;
thus f' . x = the ZeroF of (G . i) by A11
.= h' . x by A12 ; :: thesis: verum

end;

hence f = h by A13, FUNCT_1:9; :: thesis: verum