let V1, V2 be non empty strict ModuleStr over K; :: thesis:
assume that
A7: for x being set holds
( x in the carrier of V1 iff x is linear-Functional of V ) and
A8: for f, g being linear-Functional of V holds the addF of V1 . (f,g) = f + g and
A9: 0. V1 = 0Functional V and
A10: for f being linear-Functional of V
for x being Element of K holds the lmult of V1 . (x,f) = x * f and
A11: for x being set holds
( x in the carrier of V2 iff x is linear-Functional of V ) and
A12: for f, g being linear-Functional of V holds the addF of V2 . (f,g) = f + g and
A13: 0. V2 = 0Functional V and
A14: for f being linear-Functional of V
for x being Element of K holds the lmult of V2 . (x,f) = x * f ; :: thesis:

A15: now :: thesis:

let r be Element of K; :: thesis:
let x be Element of V1; :: thesis:
reconsider f = x as linear-Functional of V by A7;
thus the lmult of V1 . (r,x) = r * f by A10
.= the lmult of V2 . (r,x) by A14 ; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
thus ( x in the carrier of V1 implies x in the carrier of V2 ) :: thesis:

proof

assume x in the carrier of V1 ; :: thesis:
then x is linear-Functional of V by A7;
hence x in the carrier of V2 by A11; :: thesis:

end;

assume x in the carrier of V2 ; :: thesis:
then x is linear-Functional of V by A11;
hence x in the carrier of V1 by A7; :: thesis:

end;

then A16: the carrier of V1 = the carrier of V2 by TARSKI:2;

now :: thesis:

let x, y be Element of V1; :: thesis:
reconsider f = x, g = y as linear-Functional of V by A7;
thus the addF of V1 . (x,y) = f + g by A8
.= the addF of V2 . (x,y) by A12 ; :: thesis:

end;

then the addF of V1 = the addF of V2 by A16, BINOP_1:2;
hence V1 = V2 by A9, A13, A16, A15, BINOP_1:2; :: thesis: