let QL1, QL2 be LinearOperator of V,(VectQuot (V,W)); ( QL1 is onto & ( for v being VECTOR of V holds QL1 . v = v + W ) & QL2 is onto & ( for v being VECTOR of V holds QL2 . v = v + W ) implies QL1 = QL2 )
assume A1:
( QL1 is onto & ( for v being VECTOR of V holds QL1 . v = v + W ) )
; ( not QL2 is onto or ex v being VECTOR of V st not QL2 . v = v + W or QL1 = QL2 )
assume A2:
( QL2 is onto & ( for v being VECTOR of V holds QL2 . v = v + W ) )
; QL1 = QL2
now for v being VECTOR of V holds QL1 . v = QL2 . vlet v be
VECTOR of
V;
QL1 . v = QL2 . vthus QL1 . v =
v + W
by A1
.=
QL2 . v
by A2
;
verum end;
hence
QL1 = QL2
; verum