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 ;

hence f = h by A19; :: thesis: verum

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

( 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 = 0. (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 = 0. (g . i) by A17

.= h9 . x by A18 ; :: thesis: verum

hence f = h by A19; :: thesis: verum