let I1, I2 be LinearOperator of X,(product <*X*>); :: thesis: ( ( for x being Point of X holds I1 . x = <*x*> ) & ( for x being Point of X holds I2 . x = <*x*> ) implies I1 = I2 )
assume that
A4: for x being Point of X holds I1 . x = <*x*> and
A5: for x being Point of X holds I2 . x = <*x*> ; :: thesis: I1 = I2
for x being set st x in the carrier of X holds
I1 . x = I2 . x

proof

let x be set ; :: thesis: ( x in the carrier of X implies I1 . x = I2 . x )
assume x in the carrier of X ; :: thesis: I1 . x = I2 . x
then reconsider x1 = x as Point of X ;
thus I1 . x = <*x1*> by A4
.= I2 . x by A5 ; :: thesis: verum

end;

hence I1 = I2 ; :: thesis: verum