theorem Th24: :: ORTSP_1:24

for F being Field
for S being OrtSp of F
for a, b, c being Element of S st not b _|_ & not b _|_ holds
ProJ (c,b,a) = ((ProJ (b,a,c)) ") * (ProJ (a,b,c))