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

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

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

end;

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

end;

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

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

end;

then A20: the addF of V1 = the addF of V2 by A19, BINOP_1:2;

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

end;

hence V1 = V2 by A13, A17, A19, A20, BINOP_1:2; :: thesis: