let QL1, QL2 be LinearOperator of (VectQuot (V,(Ker L))),(Im L); :: thesis: ( QL1 is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL1 . z = L . v ) & QL2 is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL2 . z = L . v ) implies QL1 = QL2 )
assume A1: ( QL1 is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL1 . z = L . v ) ) ; :: thesis: ( not QL2 is isomorphism or ex z being Point of (VectQuot (V,(Ker L))) ex v being VECTOR of V st
( z = v + (Ker L) & not QL2 . z = L . v ) or QL1 = QL2 )
assume A2: ( QL2 is isomorphism & ( for z being Point of (VectQuot (V,(Ker L)))
for v being VECTOR of V st z = v + (Ker L) holds
QL2 . z = L . v ) ) ; :: thesis: QL1 = QL2
now :: thesis: for z being VECTOR of (VectQuot (V,(Ker L))) holds QL1 . z = QL2 . z
let z be VECTOR of (VectQuot (V,(Ker L))); :: thesis: QL1 . z = QL2 . z
consider v being Point of V such that
A3: z = v + (Ker L) by LMQ07;
thus QL1 . z = L . v by A1, A3
.= QL2 . z by A2, A3 ; :: thesis: verum
end;
hence QL1 = QL2 ; :: thesis: verum