reconsider mF = [: the carrier of F,X:] --> o as Function of [: the carrier of F,X:],X ;
consider mo being Relation of X such that
A1: for x being set holds
( x in mo iff ( x in [:X,X:] & ex a, b being Element of X st
( x = [a,b] & b = o ) ) ) by Lm2;
reconsider MPS = SymStr(# X,md,o,mF,mo #) as non empty right_complementable Abelian add-associative right_zeroed SymStr over F by Lm3;
take MPS ; :: thesis: ( MPS is OrtSp-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, d, x being Element of MPS
for l being Element of F holds
( ( a <> 0. MPS & b <> 0. MPS & c <> 0. MPS & d <> 0. MPS implies ex p being Element of MPS st
( not a _|_ & not b _|_ & not c _|_ & not d _|_ ) ) & ( 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 ; :: according to ORTSP_1:def 1 :: thesis: ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital & MPS is strict )
for a being Element of F
for x being Element of X holds mF . [a,x] = o by FUNCOP_1:7;
hence ( MPS is vector-distributive & MPS is scalar-distributive & MPS is scalar-associative & MPS is scalar-unital ) by Lm4; :: thesis: MPS is strict
thus MPS is strict ; :: thesis: verum