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

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

hence
QL1 = QL2
; :: thesis: verumlet 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;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