deffunc H2( Element of F, Element of {0}) -> Element of {0} = o;
consider mF being Function of [: the carrier of F,{0}:],{0} such that
A1:
for a being Element of F
for x being Element of {0} holds mF . (a,x) = H2(a,x)
from BINOP_1:sch 4();
consider mo being Relation of {0} such that
A2:
for x being set holds
( x in mo iff ( x in [:{0},{0}:] & ex a, b being Element of {0} st
( x = [a,b] & b = o ) ) )
by Lm2;
reconsider MPS = SymStr(# {0},md,o,mF,mo #) as non empty right_complementable Abelian add-associative right_zeroed SymStr over F by Lm3;
take
MPS
; ( MPS is SymSp-like & MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital & MPS is strict )
thus
for a, b, c, x being Element of MPS
for l being Element of F holds
( ( a <> 0. MPS implies ex y being Element of MPS st not a _|_ ) & ( b _|_ implies b _|_ ) & ( a _|_ & a _|_ implies a _|_ ) & ( not a _|_ implies ex k being Element of F st a _|_ ) & ( b + c _|_ & c + a _|_ implies a + b _|_ ) )
by A2, Lm5; SYMSP_1:def 1 ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital & MPS is strict )
thus
( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital )
by A1, Lm4; MPS is strict
thus
MPS is strict
; verum