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

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

let v be VECTOR of V; :: thesis: QL1 . v = QL2 . v
thus QL1 . v = v + W by A1
.= QL2 . v by A2 ; :: thesis: verum

end;

hence QL1 = QL2 ; :: thesis: verum