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

assume that

A5: the carrier of S1 = A and

A6: the carrier of S2 = A ; :: thesis: S1 = S2

now :: thesis: for a, b being Element of A holds the distance of S1 . (a,b) = the distance of S2 . (a,b)

hence
S1 = S2
by A5, A6, BINOP_1:2; :: thesis: verumlet 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;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