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 A1, Lm5; :: 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

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 A1, Lm5; :: 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