let QL1, QL2 be LinearOperator of V,(VectQuot (V,W)); :: thesis: ( 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 ) ) ; :: thesis: ( 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 ) ) ; :: thesis: QL1 = QL2

assume A1: ( QL1 is onto & ( for v being VECTOR of V holds QL1 . v = v + W ) ) ; :: thesis: ( 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 ) ) ; :: thesis: QL1 = QL2

now :: thesis: for v being VECTOR of V holds QL1 . v = QL2 . v

hence
QL1 = QL2
; :: thesis: verumlet v be VECTOR of V; :: thesis: QL1 . v = QL2 . v

thus QL1 . v = v + W by A1

.= QL2 . v by A2 ; :: thesis: verum

end;thus QL1 . v = v + W by A1

.= QL2 . v by A2 ; :: thesis: verum