let R be Ring; :: thesis: for V being LeftMod of R
for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
VectQuot (V,W) = VectQuot (V,Ws)
let V be LeftMod of R; :: thesis: for W being Subspace of V
for Ws being strict Subspace of V st Ws = (Omega). W holds
VectQuot (V,W) = VectQuot (V,Ws)
let W be Subspace of V; :: thesis: for Ws being strict Subspace of V st Ws = (Omega). W holds
VectQuot (V,W) = VectQuot (V,Ws)
let Ws be strict Subspace of V; :: thesis: ( Ws = (Omega). W implies VectQuot (V,W) = VectQuot (V,Ws) )
assume A1: Ws = (Omega). W ; :: thesis: VectQuot (V,W) = VectQuot (V,Ws)
set Z1 = VectQuot (V,W);
set Z2 = VectQuot (V,Ws);
A2: the carrier of (VectQuot (V,W)) = CosetSet (V,W) by VECTSP10:def 6
.= CosetSet (V,Ws) by A1, LmStrict1
.= the carrier of (VectQuot (V,Ws)) by VECTSP10:def 6 ;
A3: the addF of (VectQuot (V,W)) = addCoset (V,W) by VECTSP10:def 6
.= addCoset (V,Ws) by A1, LmStrict2
.= the addF of (VectQuot (V,Ws)) by VECTSP10:def 6 ;
A4: 0. (VectQuot (V,W)) = zeroCoset (V,W) by VECTSP10:def 6
.= zeroCoset (V,Ws) by A1
.= 0. (VectQuot (V,Ws)) by VECTSP10:def 6 ;
the lmult of (VectQuot (V,W)) = lmultCoset (V,W) by VECTSP10:def 6
.= lmultCoset (V,Ws) by A1, LmStrict3
.= the lmult of (VectQuot (V,Ws)) by VECTSP10:def 6 ;
hence VectQuot (V,W) = VectQuot (V,Ws) by A2, A3, A4; :: thesis: verum