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 of F by Lm3;
take MPS ; :: thesis: ( MPS is SymSp-like & MPS is VectSp-like & 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 VectSp-like & MPS is strict )
thus MPS is VectSp-like by A1, Lm4; :: thesis: MPS is strict
thus MPS is strict ; :: thesis: verum