let S1, S2 be strict SubSpace of M; :: thesis: ( the carrier of S1 = A & the carrier of S2 = A implies S1 = S2 )
assume that
A5: the carrier of S1 = A and
A6: the carrier of S2 = A ; :: thesis: S1 = S2

now

let a, b be Element of A; :: thesis: the distance of S1 . a,b = the distance of S2 . a,b
thus the distance of S1 . a,b = the distance of M . a,b by A5, Def1
.= the distance of S2 . a,b by A6, Def1 ; :: thesis: verum

end;

hence S1 = S2 by A5, A6, BINOP_1:2; :: thesis: verum