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 ;

hence f = h by A19, FUNCT_1:2; :: thesis: verum

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 :: thesis: for x being object st x in dom (carr G) holds

f9 . x = h9 . x

( dom f9 = dom (carr G) & dom h9 = dom (carr G) )
by CARD_3:9;f9 . x = h9 . x

let x be object ; :: 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;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

hence f = h by A19, FUNCT_1:2; :: thesis: verum