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
A11: for i being Element of dom (carr g) holds f . i = 0. (g . i) and
A12: for i being Element of dom (carr g) holds h . i = 0. (g . i) ; :: 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 = 0. (g . i) by A11
.= h' . x by A12 ; :: thesis: verum

end;

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