let f1, f2 be linear-transformation of V,(VectQuot (V,W)); :: thesis: ( ( for v being Element of V holds f1 . v = v + W ) & ( for v being Element of V holds f2 . v = v + W ) implies f1 = f2 )
assume AS1: for v being Element of V holds f1 . v = v + W ; :: thesis: ( ex v being Element of V st not f2 . v = v + W or f1 = f2 )
assume AS2: for v being Element of V holds f2 . v = v + W ; :: thesis: f1 = f2
for v being Element of V holds f1 . v = f2 . v

proof

let v be Element of V; :: thesis: f1 . v = f2 . v
thus f1 . v = v + W by AS1
.= f2 . v by AS2 ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:def 8; :: thesis: verum