let f, h be Element of product (carr g); :: thesis: ( ( for i being Element of dom (carr g) holds f . i = 0. (g . i) ) & ( for i being Element of dom (carr g) holds h . i = 0. (g . i) ) implies f = h )
assume that
A17: for i being Element of dom (carr g) holds f . i = 0. (g . i) and
A18: for i being Element of dom (carr g) holds h . i = 0. (g . i) ; :: thesis: f = h
reconsider f' = f, h' = h as Function ;

A19: 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 = 0. (g . i) by A17
.= h' . x by A18 ; :: thesis: verum

end;

( dom f' = dom (carr g) & dom h' = dom (carr g) ) by CARD_3:18;
hence f = h by A19, FUNCT_1:9; :: thesis: verum