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 f9 = f, h9 = h as Function ;
A19: now :: thesis: for x being object st x in dom (carr g) holds
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 = 0. (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; :: thesis: verum