0Functional V in { x where x is linear-Functional of V : verum } ;
then reconsider ca = { x where x is linear-Functional of V : verum } as non empty set ;

A1: now

let x be set ; :: thesis: ( ( x in ca implies x is linear-Functional of V ) & ( x is linear-Functional of V implies x in ca ) )
thus ( x in ca implies x is linear-Functional of V ) :: thesis: ( x is linear-Functional of V implies x in ca )

proof

assume x in ca ; :: thesis: x is linear-Functional of V
then consider y being linear-Functional of V such that
A2: x = y ;
thus x is linear-Functional of V by A2; :: thesis: verum

end;

thus ( x is linear-Functional of V implies x in ca ) ; :: thesis: verum

end;

defpred S₁[ set , set , set ] means ex f, g being Functional of V st
( $1 = f & $2 = g & $3 = f + g );
A3: for x, y being Element of ca ex u being Element of ca st S₁[x,y,u]

proof

let x, y be Element of ca; :: thesis: ex u being Element of ca st S₁[x,y,u]
reconsider f = x, g = y as linear-Functional of V by A1;
reconsider u = f + g as Element of ca by A1;
take u ; :: thesis: S₁[x,y,u]
take f ; :: thesis: ex g being Functional of V st
( x = f & y = g & u = f + g )
take g ; :: thesis: ( x = f & y = g & u = f + g )
thus ( x = f & y = g & u = f + g ) ; :: thesis: verum

end;

consider ad being Function of [:ca,ca:],ca such that
A4: for x, y being Element of ca holds S₁[x,y,ad . x,y] from BINOP_1:sch 3(A3);

A5: now

let f, g be linear-Functional of V; :: thesis: ad . f,g = f + g
reconsider x = f, y = g as Element of ca by A1;
consider f1, g1 being Functional of V such that
A6: ( x = f1 & y = g1 & ad . x,y = f1 + g1 ) by A4;
thus ad . f,g = f + g by A6; :: thesis: verum

end;

reconsider 0F = 0Functional V as Element of ca by A1;
defpred S₂[ Element of K, set , set ] means ex f being Functional of V st
( $2 = f & $3 = $1 * f );
A7: for x being Element of K
for y being Element of ca ex u being Element of ca st S₂[x,y,u]

proof

let x be Element of K; :: thesis: for y being Element of ca ex u being Element of ca st S₂[x,y,u]
let y be Element of ca; :: thesis: ex u being Element of ca st S₂[x,y,u]
reconsider f = y as linear-Functional of V by A1;
reconsider u = x * f as Element of ca by A1;
take u ; :: thesis: S₂[x,y,u]
take f ; :: thesis: ( y = f & u = x * f )
thus ( y = f & u = x * f ) ; :: thesis: verum

end;

consider lm being Function of [:the carrier of K,ca:],ca such that
A8: for x being Element of K
for y being Element of ca holds S₂[x,y,lm . x,y] from BINOP_1:sch 3(A7);

A9: now

let f be linear-Functional of V; :: thesis: for x being Element of K holds lm . x,f = x * f
let x be Element of K; :: thesis: lm . x,f = x * f
reconsider y = f as Element of ca by A1;
consider f1 being Functional of V such that
A10: ( y = f1 & lm . x,y = x * f1 ) by A8;
thus lm . x,f = x * f by A10; :: thesis: verum

end;

reconsider V1 = VectSpStr(# ca,ad,0F,lm #) as non empty strict VectSpStr of K ;
take V1 ; :: thesis: ( ( for x being set holds
( x in the carrier of V1 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of V1 . f,g = f + g ) & 0. V1 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of V1 . x,f = x * f ) )
thus ( ( for x being set holds
( x in the carrier of V1 iff x is linear-Functional of V ) ) & ( for f, g being linear-Functional of V holds the addF of V1 . f,g = f + g ) & 0. V1 = 0Functional V & ( for f being linear-Functional of V
for x being Element of K holds the lmult of V1 . x,f = x * f ) ) by A1, A5, A9; :: thesis: verum