defpred S₁[ set , set , set ] means ex f, g being Functional of V st
( $1 = f & $2 = g & $3 = f + g );
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 :: thesis: for x being set holds
( ( x in ca implies x is linear-Functional of V ) & ( x is linear-Functional of V implies x in ca ) )

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 ex y being linear-Functional of V st x = y ;
hence x is linear-Functional of V ; :: thesis: verum

end;

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

end;

then reconsider 0F = 0Functional V as Element of ca ;
A2: 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
A3: for x, y being Element of ca holds S₁[x,y,ad . (x,y)] from BINOP_1:sch 3(A2);
defpred S₂[ Element of K, set , set ] means ex f being Functional of V st
( $2 = f & $3 = $1 * f );
A4: 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
A5: for x being Element of K
for y being Element of ca holds S₂[x,y,lm . (x,y)] from BINOP_1:sch 3(A4);

A6: now :: thesis: for f being linear-Functional of V
for x being Element of K holds lm . (x,f) = x * f

let f be linear-Functional of V; :: thesis: for x being Element of K holds lm . (x,f) = x * f
reconsider y = f as Element of ca by A1;
let x be Element of K; :: thesis: lm . (x,f) = x * f
ex f1 being Functional of V st
( y = f1 & lm . (x,y) = x * f1 ) by A5;
hence lm . (x,f) = x * f ; :: thesis: verum

end;

reconsider V1 = ModuleStr(# ca,ad,0F,lm #) as non empty strict ModuleStr over 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 ) )

now :: thesis: for f, g being linear-Functional of V holds ad . (f,g) = f + g

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;
ex f1, g1 being Functional of V st
( x = f1 & y = g1 & ad . (x,y) = f1 + g1 ) by A3;
hence ad . (f,g) = f + g ; :: thesis: verum

end;

hence ( ( 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, A6; :: thesis: verum