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 )

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

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 RLSp2RVSp Y
; :: thesis: x is Coset of Yassume
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;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

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