deffunc H₂( 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) = H₂(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 ; :: thesis: ( 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; :: according to SYMSP_1:def 1 :: thesis: ( 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; :: thesis: MPS is strict
thus MPS is strict ; :: thesis: verum