let X be RealLinearSpace; :: thesis: for Y being Subspace of X holds CosetSet (X,Y) = CosetSet ((RLSp2RVSp X),(RLSp2RVSp Y))
let Y be Subspace of X; :: thesis: CosetSet (X,Y) = CosetSet ((RLSp2RVSp X),(RLSp2RVSp Y))
for x being object holds
( x in CosetSet (X,Y) iff x in CosetSet ((RLSp2RVSp X),(RLSp2RVSp Y)) )
proof
let x be object ; :: thesis: ( x in CosetSet (X,Y) iff x in CosetSet ((RLSp2RVSp X),(RLSp2RVSp Y)) )
hereby :: thesis: ( x in CosetSet ((RLSp2RVSp X),(RLSp2RVSp Y)) implies x in CosetSet (X,Y) )
assume x in CosetSet (X,Y) ; :: thesis: x in CosetSet ((RLSp2RVSp X),(RLSp2RVSp Y))
then consider A being Coset of Y such that
A1: x = A ;
x is Coset of RLSp2RVSp Y by A1, LMQ04;
hence x in CosetSet ((RLSp2RVSp X),(RLSp2RVSp Y)) ; :: thesis: verum
end;
assume x in CosetSet ((RLSp2RVSp X),(RLSp2RVSp Y)) ; :: thesis: x in CosetSet (X,Y)
then consider B being Coset of RLSp2RVSp Y such that
A2: x = B ;
x is Coset of Y by A2, LMQ04;
hence x in CosetSet (X,Y) ; :: thesis: verum
end;
hence CosetSet (X,Y) = CosetSet ((RLSp2RVSp X),(RLSp2RVSp Y)) by TARSKI:2; :: thesis: verum