let X be RealLinearSpace; :: thesis: for Y being Subspace of X
for x being object holds
( x is Coset of Y iff x is Coset of RLSp2RVSp Y )
let Y be Subspace of X; :: thesis: for x being object holds
( x is Coset of Y iff x is Coset of RLSp2RVSp Y )
let x be object ; :: thesis: ( x is Coset of Y iff x is Coset of RLSp2RVSp Y )
hereby :: thesis: ( x is Coset of RLSp2RVSp Y implies x is Coset of Y )
assume x is Coset of Y ; :: thesis: x is Coset of RLSp2RVSp Y
then consider v being Element of X such that
A1: x = v + Y by RLSUB_1:def 6;
reconsider v1 = v as Element of (RLSp2RVSp X) ;
x = v1 + (RLSp2RVSp Y) by A1, LMQ03;
hence x is Coset of RLSp2RVSp Y by VECTSP_4:def 6; :: thesis: verum
end;
assume x is Coset of RLSp2RVSp Y ; :: thesis: x is Coset of Y
then consider v1 being Element of (RLSp2RVSp X) such that
A2: x = v1 + (RLSp2RVSp Y) by VECTSP_4:def 6;
reconsider v = v1 as Element of X ;
x = v + Y by A2, LMQ03;
hence x is Coset of Y by RLSUB_1:def 6; :: thesis: verum