:: ORTSP_1 semantic presentation

reconsider c1 = {0} as non empty set ;

reconsider c2 = 0 as Element of c1 by TARSKI:def 1;

deffunc H1( Element of c1, Element of c1) -> Element of c1 = c2;

consider c3 being BinOp of c1 such that
Lemma1: for b1, b2 being Element of c1 holds c3 . b1,b2 = H1(b1,b2) from BINOP_1:sch 2();

E2: now
let c4 be Field;
set c5 = [:c1,c1:];
defpred S1[ set ] means ex b1, b2 being Element of c1 st
( a1 = [b1,b2] & b2 = c2 );
consider c6 being set such that
E3: for b1 being set holds
( b1 in c6 iff ( b1 in [:c1,c1:] & S1[b1] ) ) from XBOOLE_0:sch 1();
 c6 c= [:c1,c1:]
proof
let c7 be set ; :: according to TARSKI:def 3
thus ( not c7 in c6 or c7 in [:c1,c1:] ) by E3;
end;
then reconsider c7 = c6 as Relation of c1 by RELSET_1:def 1;
take c8 = c7;
thus for b1 being set holds
( b1 in c8 iff ( b1 in [:c1,c1:] & ex b2, b3 being Element of c1 st
( b1 = [b2,b3] & b3 = c2 ) ) ) by E3;
end;

Lemma3: for b1 being Field
for b2 being Function of [:the carrier of b1,c1:],c1
for b3 being Relation of c1 holds
( SymStr(# c1,c3,c2,b2,b3 #) is Abelian & SymStr(# c1,c3,c2,b2,b3 #) is add-associative & SymStr(# c1,c3,c2,b2,b3 #) is right_zeroed & SymStr(# c1,c3,c2,b2,b3 #) is right_complementable )
proof end;

E4: now
let c4 be Field;
let c5 be Function of [:the carrier of c4,c1:],c1;
assume E5: for b1 being Element of c4
for b2 being Element of c1 holds c5 . [b1,b2] = c2 ;
let c6 be Relation of c1;
let c7 be non empty Abelian add-associative right_zeroed right_complementable SymStr of c4;
assume E6: c7 = SymStr(# c1,c3,c2,c5,c6 #) ;
thus c7 is VectSp-like
proof
for b1, b2 being Element of c4
for b3, b4 being Element of c7 holds
( b1 * (b3 + b4) = (b1 * b3) + (b1 * b4) & (b1 + b2) * b3 = (b1 * b3) + (b2 * b3) & (b1 * b2) * b3 = b1 * (b2 * b3) & (1. c4) * b3 = b3 )
proof
let c8, c9 be Element of c4;
let c10, c11 be Element of c7;
E7: c8 * (c10 + c11) = (c8 * c10) + (c8 * c11)
proof
reconsider c12 = c10, c13 = c11 as Element of c7 ;
E8: c12 + c13 = c3 . c12,c13 by E6, RLVECT_1:5;
reconsider c14 = c12, c15 = c13 as Element of c1 by E6;
E9: c3 . c14,c15 = c2 by Lemma1;
reconsider c16 = c14, c17 = c15 as Element of c7 ;
E10: c8 * (c16 + c17) = c5 . c8,c2 by E6, E8, E9, VECTSP_1:def 24;
E11: c8 * (c16 + c17) = c2 by E5, E10;
reconsider c18 = c16 as Element of c7 ;
E12: c5 . c8,c18 = c2 by E5;
reconsider c19 = c18 as Element of c7 ;
E13: c8 * c19 = c2 by E6, E12, VECTSP_1:def 24;
reconsider c20 = c17 as Element of c7 ;
E14: c5 . c8,c20 = c2 by E5;
reconsider c21 = c20 as Element of c7 ;
E15: c8 * c21 = c2 by E6, E14, VECTSP_1:def 24;
c2 = 0. c7 by E6, RLVECT_1:def 2;
hence c8 * (c10 + c11) = (c8 * c10) + (c8 * c11) by E11, E13, E15, RLVECT_1:10;
end;
E8: (c8 + c9) * c10 = (c8 * c10) + (c9 * c10)
proof
set c12 = c8 + c9;
E9: (c8 + c9) * c10 = c5 . (c8 + c9),c10 by E6, VECTSP_1:def 24;
reconsider c13 = c10 as Element of c7 ;
reconsider c14 = c13 as Element of c7 ;
E10: (c8 + c9) * c14 = c2 by E5, E6, E9;
reconsider c15 = c14 as Element of c7 ;
E11: c5 . c8,c15 = c2 by E5, E6;
reconsider c16 = c15 as Element of c7 ;
E12: c8 * c16 = c2 by E6, E11, VECTSP_1:def 24;
reconsider c17 = c16 as Element of c7 ;
E13: c5 . c9,c17 = c2 by E5, E6;
reconsider c18 = c17 as Element of c7 ;
E14: c9 * c18 = c2 by E6, E13, VECTSP_1:def 24;
c2 = 0. c7 by E6, RLVECT_1:def 2;
hence (c8 + c9) * c10 = (c8 * c10) + (c9 * c10) by E10, E12, E14, RLVECT_1:10;
end;
E9: (c8 * c9) * c10 = c8 * (c9 * c10)
proof
set c12 = c8 * c9;
E10: (c8 * c9) * c10 = c5 . (c8 * c9),c10 by E6, VECTSP_1:def 24;
reconsider c13 = c10 as Element of c7 ;
reconsider c14 = c13 as Element of c7 ;
E11: (c8 * c9) * c14 = c2 by E5, E6, E10;
reconsider c15 = c14 as Element of c7 ;
E12: c5 . c9,c15 = c2 by E5, E6;
reconsider c16 = c15 as Element of c7 ;
c9 * c16 = c2 by E6, E12, VECTSP_1:def 24;
then E13: c8 * (c9 * c16) = c5 . c8,c2 by E6, VECTSP_1:def 24;
thus (c8 * c9) * c10 = c8 * (c9 * c10) by E5, E11, E13;
end;
(1. c4) * c10 = c10
proof
set c12 = 1. c4;
E10: (1. c4) * c10 = c5 . (1. c4),c10 by E6, VECTSP_1:def 24;
reconsider c13 = c10 as Element of c7 ;
c5 . (1. c4),c13 = c2 by E5, E6;
hence (1. c4) * c10 = c10 by E6, E10, TARSKI:def 1;
end;
hence ( c8 * (c10 + c11) = (c8 * c10) + (c8 * c11) & (c8 + c9) * c10 = (c8 * c10) + (c9 * c10) & (c8 * c9) * c10 = c8 * (c9 * c10) & (1. c4) * c10 = c10 ) by E7, E8, E9;
end;
hence c7 is VectSp-like by VECTSP_1:def 26;
end;
end;

E5: now
let c4 be Field;
let c5 be Function of [:the carrier of c4,c1:],c1;
assume for b1 being Element of c4
for b2 being Element of c1 holds c5 . [b1,b2] = c2 ;
set c6 = [:c1,c1:];
let c7 be Relation of c1;
assume E6: for b1 being set holds
( b1 in c7 iff ( b1 in [:c1,c1:] & ex b2, b3 being Element of c1 st
( b1 = [b2,b3] & b3 = c2 ) ) ) ;
let c8 be non empty Abelian add-associative right_zeroed right_complementable SymStr of c4;
assume E7: c8 = SymStr(# c1,c3,c2,c5,c7 #) ;
E8: for b1, b2 being Element of c8 holds
( b1 _|_ b2 iff ( [b1,b2] in [:c1,c1:] & ex b3, b4 being Element of c1 st
( [b1,b2] = [b3,b4] & b4 = c2 ) ) )
proof
let c9, c10 be Element of c8;
( c9 _|_ c10 iff [c9,c10] in c7 ) by E7, SYMSP_1:def 1;
hence ( c9 _|_ c10 iff ( [c9,c10] in [:c1,c1:] & ex b1, b2 being Element of c1 st
( [c9,c10] = [b1,b2] & b2 = c2 ) ) ) by E6;
end;
E9: for b1, b2 being Element of c8 holds
( b1 _|_ b2 iff b2 = c2 )
proof
let c9, c10 be Element of c8;
E10: ( c9 _|_ c10 implies c10 = c2 )
proof
assume c9 _|_ c10 ;
then ex b1, b2 being Element of c1 st
( [c9,c10] = [b1,b2] & b2 = c2 ) by E8;
hence c10 = c2 by ZFMISC_1:33;
end;
( c10 = c2 implies c9 _|_ c10 )
proof
assume E11: c10 = c2 ;
consider c11, c12 being Element of c8 such that
E12: ( c11 = c9 & c12 = c10 ) ;
[c9,c10] = [c11,c12] by E12;
hence c9 _|_ c10 by E7, E8, E11;
end;
hence ( c9 _|_ c10 iff c10 = c2 ) by E10;
end;
0. c8 = c2 by E7, TARSKI:def 1;
hence for b1, b2, b3, b4 being Element of c8 st b1 <> 0. c8 & b2 <> 0. c8 & b3 <> 0. c8 & b4 <> 0. c8 holds
ex b5 being Element of c8 st
( not b5 _|_ b1 & not b5 _|_ b2 & not b5 _|_ b3 & not b5 _|_ b4 ) by E7, TARSKI:def 1;
thus for b1, b2 being Element of c8
for b3 being Element of c4 st b1 _|_ b2 holds
b3 * b1 _|_ b2
proof
let c9, c10 be Element of c8;
let c11 be Element of c4;
assume c9 _|_ c10 ;
then c10 = c2 by E9;
hence c11 * c9 _|_ c10 by E9;
end;
thus for b1, b2, b3 being Element of c8 st b2 _|_ b1 & b3 _|_ b1 holds
b2 + b3 _|_ b1
proof
let c9, c10, c11 be Element of c8;
assume ( c10 _|_ c9 & c11 _|_ c9 ) ;
then c9 = c2 by E9;
hence c10 + c11 _|_ c9 by E9;
end;
thus for b1, b2, b3 being Element of c8 st not b2 _|_ b1 holds
ex b4 being Element of c4 st b3 - (b4 * b2) _|_ b1
proof
let c9, c10, c11 be Element of c8;
assume E10: not c10 _|_ c9 ;
assume for b1 being Element of c4 holds not c11 - (b1 * c10) _|_ c9 ;
c9 <> c2 by E9, E10;
hence contradiction by E7, TARSKI:def 1;
end;
thus for b1, b2, b3 being Element of c8 st b1 _|_ b2 - b3 & b2 _|_ b3 - b1 holds
b3 _|_ b1 - b2
proof
let c9, c10, c11 be Element of c8;
assume ( c9 _|_ c10 - c11 & c10 _|_ c11 - c9 ) ;
assume not c11 _|_ c9 - c10 ;
then c9 - c10 <> c2 by E9;
hence contradiction by E7, TARSKI:def 1;
end;
end;

definition
let c4 be Field;
let c5 be non empty Abelian add-associative right_zeroed right_complementable SymStr of c4;
canceled;
attr a2 is OrtSp-like means :Def2: :: ORTSP_1:def 2
for b1, b2, b3, b4, b5 being Element of a2
for b6 being Element of a1 holds
( ( b1 <> 0. a2 & b2 <> 0. a2 & b3 <> 0. a2 & b4 <> 0. a2 implies ex b7 being Element of a2 st
( not b7 _|_ b1 & not b7 _|_ b2 & not b7 _|_ b3 & not b7 _|_ b4 ) ) & ( b1 _|_ b2 implies b6 * b1 _|_ b2 ) & ( b2 _|_ b1 & b3 _|_ b1 implies b2 + b3 _|_ b1 ) & ( not b2 _|_ b1 implies ex b7 being Element of a1 st b5 - (b7 * b2) _|_ b1 ) & ( b1 _|_ b2 - b3 & b2 _|_ b3 - b1 implies b3 _|_ b1 - b2 ) );
end;

:: deftheorem Def1 ORTSP_1:def 1 :
canceled;

:: deftheorem Def2 defines OrtSp-like ORTSP_1:def 2 :
for b1 being Field
for b2 being non empty Abelian add-associative right_zeroed right_complementable SymStr of b1 holds
( b2 is OrtSp-like iff for b3, b4, b5, b6, b7 being Element of b2
for b8 being Element of b1 holds
( ( b3 <> 0. b2 & b4 <> 0. b2 & b5 <> 0. b2 & b6 <> 0. b2 implies ex b9 being Element of b2 st
( not b9 _|_ b3 & not b9 _|_ b4 & not b9 _|_ b5 & not b9 _|_ b6 ) ) & ( b3 _|_ b4 implies b8 * b3 _|_ b4 ) & ( b4 _|_ b3 & b5 _|_ b3 implies b4 + b5 _|_ b3 ) & ( not b4 _|_ b3 implies ex b9 being Element of b1 st b7 - (b9 * b4) _|_ b3 ) & ( b3 _|_ b4 - b5 & b4 _|_ b5 - b3 implies b5 _|_ b3 - b4 ) ) );

registration
let c4 be Field;
cluster non empty Abelian add-associative right_zeroed right_complementable VectSp-like strict OrtSp-like SymStr of a1;
existence
ex b1 being non empty Abelian add-associative right_zeroed right_complementable SymStr of c4 st
( b1 is OrtSp-like & b1 is VectSp-like & b1 is strict )
proof end;
end;

definition
let c4 be Field;
mode OrtSp of a1 is non empty Abelian add-associative right_zeroed right_complementable VectSp-like OrtSp-like SymStr of a1;
end;

theorem Th1: :: ORTSP_1:1
canceled;

theorem Th2: :: ORTSP_1:2
canceled;

theorem Th3: :: ORTSP_1:3
canceled;

theorem Th4: :: ORTSP_1:4
canceled;

theorem Th5: :: ORTSP_1:5
canceled;

theorem Th6: :: ORTSP_1:6
canceled;

theorem Th7: :: ORTSP_1:7
canceled;

theorem Th8: :: ORTSP_1:8
canceled;

theorem Th9: :: ORTSP_1:9
canceled;

theorem Th10: :: ORTSP_1:10
canceled;

theorem Th11: :: ORTSP_1:11
for b1 being Field
for b2 being OrtSp of b1
for b3 being Element of b2 holds 0. b2 _|_ b3
proof end;

theorem Th12: :: ORTSP_1:12
for b1 being Field
for b2 being OrtSp of b1
for b3, b4 being Element of b2 st b3 _|_ b4 holds
b4 _|_ b3
proof end;

theorem Th13: :: ORTSP_1:13
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 & b5 + b3 _|_ b4 holds
not b5 _|_ b4
proof end;

theorem Th14: :: ORTSP_1:14
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 & b5 _|_ b4 holds
not b3 + b5 _|_ b4
proof end;

theorem Th15: :: ORTSP_1:15
for b1 being Field
for b2 being OrtSp of b1
for b3, b4 being Element of b2
for b5 being Element of b1 st not b3 _|_ b4 & not b5 = 0. b1 holds
( not b5 * b3 _|_ b4 & not b3 _|_ b5 * b4 )
proof end;

theorem Th16: :: ORTSP_1:16
for b1 being Field
for b2 being OrtSp of b1
for b3, b4 being Element of b2 st b3 _|_ b4 holds
- b3 _|_ b4
proof end;

theorem Th17: :: ORTSP_1:17
canceled;

theorem Th18: :: ORTSP_1:18
canceled;

theorem Th19: :: ORTSP_1:19
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6 being Element of b2 st b3 - b4 _|_ b5 & b3 - b6 _|_ b5 holds
b4 - b6 _|_ b5
proof end;

theorem Th20: :: ORTSP_1:20
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2
for b6, b7 being Element of b1 st not b3 _|_ b4 & b5 - (b6 * b3) _|_ b4 & b5 - (b7 * b3) _|_ b4 holds
b6 = b7
proof end;

theorem Th21: :: ORTSP_1:21
for b1 being Field
for b2 being OrtSp of b1
for b3, b4 being Element of b2 st b3 _|_ b3 & b4 _|_ b4 holds
b3 + b4 _|_ b3 - b4
proof end;

theorem Th22: :: ORTSP_1:22
for b1 being Field
for b2 being OrtSp of b1 st (1. b1) + (1. b1) <> 0. b1 & ex b3 being Element of b2 st b3 <> 0. b2 holds
ex b3 being Element of b2 st not b3 _|_ b3
proof end;

definition
let c4 be Field;
let c5 be OrtSp of c4;
let c6, c7, c8 be Element of c5;
assume E16: not c7 _|_ c6 ;
canceled;
canceled;
canceled;
func ProJ c3,c4,c5 -> Element of a1 means :Def6: :: ORTSP_1:def 6
for b1 being Element of a1 st a5 - (b1 * a4) _|_ a3 holds
a6 = b1;
existence
ex b1 being Element of c4 st
for b2 being Element of c4 st c8 - (b2 * c7) _|_ c6 holds
b1 = b2
proof end;
uniqueness
for b1, b2 being Element of c4 st ( for b3 being Element of c4 st c8 - (b3 * c7) _|_ c6 holds
b1 = b3 ) & ( for b3 being Element of c4 st c8 - (b3 * c7) _|_ c6 holds
b2 = b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 ORTSP_1:def 3 :
canceled;

:: deftheorem Def4 ORTSP_1:def 4 :
canceled;

:: deftheorem Def5 ORTSP_1:def 5 :
canceled;

:: deftheorem Def6 defines ProJ ORTSP_1:def 6 :
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2 st not b4 _|_ b3 holds
for b6 being Element of b1 holds
( b6 = ProJ b3,b4,b5 iff for b7 being Element of b1 st b5 - (b7 * b4) _|_ b3 holds
b6 = b7 );

theorem Th23: :: ORTSP_1:23
canceled;

theorem Th24: :: ORTSP_1:24
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 holds
b5 - ((ProJ b4,b3,b5) * b3) _|_ b4
proof end;

theorem Th25: :: ORTSP_1:25
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2
for b6 being Element of b1 st not b3 _|_ b4 holds
ProJ b4,b3,(b6 * b5) = b6 * (ProJ b4,b3,b5)
proof end;

theorem Th26: :: ORTSP_1:26
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 holds
ProJ b4,b3,(b5 + b6) = (ProJ b4,b3,b5) + (ProJ b4,b3,b6)
proof end;

theorem Th27: :: ORTSP_1:27
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2
for b6 being Element of b1 st not b3 _|_ b4 & b6 <> 0. b1 holds
ProJ b4,(b6 * b3),b5 = (b6 " ) * (ProJ b4,b3,b5)
proof end;

theorem Th28: :: ORTSP_1:28
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2
for b6 being Element of b1 st not b3 _|_ b4 & b6 <> 0. b1 holds
ProJ (b6 * b4),b3,b5 = ProJ b4,b3,b5
proof end;

theorem Th29: :: ORTSP_1:29
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 & b5 _|_ b4 holds
( ProJ b4,(b3 + b5),b6 = ProJ b4,b3,b6 & ProJ b4,b3,(b6 + b5) = ProJ b4,b3,b6 )
proof end;

theorem Th30: :: ORTSP_1:30
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 & b5 _|_ b3 & b5 _|_ b6 holds
ProJ (b4 + b5),b3,b6 = ProJ b4,b3,b6
proof end;

theorem Th31: :: ORTSP_1:31
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 & b5 - b3 _|_ b4 holds
ProJ b4,b3,b5 = 1. b1
proof end;

theorem Th32: :: ORTSP_1:32
for b1 being Field
for b2 being OrtSp of b1
for b3, b4 being Element of b2 st not b3 _|_ b4 holds
ProJ b4,b3,b3 = 1. b1
proof end;

theorem Th33: :: ORTSP_1:33
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 holds
( b5 _|_ b4 iff ProJ b4,b3,b5 = 0. b1 )
proof end;

theorem Th34: :: ORTSP_1:34
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 & not b5 _|_ b4 holds
(ProJ b4,b3,b6) * ((ProJ b4,b3,b5) " ) = ProJ b4,b5,b6
proof end;

theorem Th35: :: ORTSP_1:35
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 & not b5 _|_ b4 holds
ProJ b4,b3,b5 = (ProJ b4,b5,b3) "
proof end;

theorem Th36: :: ORTSP_1:36
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 & b3 _|_ b5 + b4 holds
ProJ b4,b3,b5 = - (ProJ b5,b3,b4)
proof end;

theorem Th37: :: ORTSP_1:37
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5 being Element of b2 st not b3 _|_ b4 & not b5 _|_ b4 holds
ProJ b5,b4,b3 = ((ProJ b4,b3,b5) " ) * (ProJ b3,b4,b5)
proof end;

theorem Th38: :: ORTSP_1:38
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 & not b3 _|_ b5 & not b6 _|_ b4 & not b6 _|_ b5 holds
(ProJ b4,b6,b3) * (ProJ b3,b4,b5) = (ProJ b6,b4,b5) * (ProJ b5,b6,b3)
proof end;

theorem Th39: :: ORTSP_1:39
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6, b7, b8 being Element of b2 st not b3 _|_ b4 & not b3 _|_ b5 & not b6 _|_ b4 & not b6 _|_ b5 & not b7 _|_ b4 holds
((ProJ b4,b7,b3) * (ProJ b3,b4,b5)) * (ProJ b5,b3,b8) = ((ProJ b4,b7,b6) * (ProJ b6,b4,b5)) * (ProJ b5,b6,b8)
proof end;

theorem Th40: :: ORTSP_1:40
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 & not b5 _|_ b4 & not b6 _|_ b4 holds
(ProJ b4,b3,b5) * (ProJ b5,b4,b6) = (ProJ b4,b3,b6) * (ProJ b6,b4,b5)
proof end;

definition
let c4 be Field;
let c5 be OrtSp of c4;
let c6, c7, c8, c9 be Element of c5;
assume E31: not c9 _|_ c8 ;
func PProJ c5,c6,c3,c4 -> Element of a1 means :Def7: :: ORTSP_1:def 7
for b1 being Element of a2 st not b1 _|_ a5 & not b1 _|_ a3 holds
a7 = ((ProJ a5,a6,b1) * (ProJ b1,a5,a3)) * (ProJ a3,b1,a4) if ex b1 being Element of a2 st
( not b1 _|_ a5 & not b1 _|_ a3 )
a7 = 0. a1 if for b1 being Element of a2 holds
( b1 _|_ a5 or b1 _|_ a3 )
;
existence
( ( ex b1 being Element of c5 st
( not b1 _|_ c8 & not b1 _|_ c6 ) implies ex b1 being Element of c4 st
for b2 being Element of c5 st not b2 _|_ c8 & not b2 _|_ c6 holds
b1 = ((ProJ c8,c9,b2) * (ProJ b2,c8,c6)) * (ProJ c6,b2,c7) ) & ( ( for b1 being Element of c5 holds
( b1 _|_ c8 or b1 _|_ c6 ) ) implies ex b1 being Element of c4 st b1 = 0. c4 ) )
proof end;
uniqueness
for b1, b2 being Element of c4 holds
( ( ex b3 being Element of c5 st
( not b3 _|_ c8 & not b3 _|_ c6 ) & ( for b3 being Element of c5 st not b3 _|_ c8 & not b3 _|_ c6 holds
b1 = ((ProJ c8,c9,b3) * (ProJ b3,c8,c6)) * (ProJ c6,b3,c7) ) & ( for b3 being Element of c5 st not b3 _|_ c8 & not b3 _|_ c6 holds
b2 = ((ProJ c8,c9,b3) * (ProJ b3,c8,c6)) * (ProJ c6,b3,c7) ) implies b1 = b2 ) & ( ( for b3 being Element of c5 holds
( b3 _|_ c8 or b3 _|_ c6 ) ) & b1 = 0. c4 & b2 = 0. c4 implies b1 = b2 ) )
proof end;
consistency
for b1 being Element of c4 st ex b2 being Element of c5 st
( not b2 _|_ c8 & not b2 _|_ c6 ) & ( for b2 being Element of c5 holds
( b2 _|_ c8 or b2 _|_ c6 ) ) holds
( ( for b2 being Element of c5 st not b2 _|_ c8 & not b2 _|_ c6 holds
b1 = ((ProJ c8,c9,b2) * (ProJ b2,c8,c6)) * (ProJ c6,b2,c7) ) iff b1 = 0. c4 ) ;
end;

:: deftheorem Def7 defines PProJ ORTSP_1:def 7 :
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6 being Element of b2 st not b6 _|_ b5 holds
for b7 being Element of b1 holds
( ( ex b8 being Element of b2 st
( not b8 _|_ b5 & not b8 _|_ b3 ) implies ( b7 = PProJ b5,b6,b3,b4 iff for b8 being Element of b2 st not b8 _|_ b5 & not b8 _|_ b3 holds
b7 = ((ProJ b5,b6,b8) * (ProJ b8,b5,b3)) * (ProJ b3,b8,b4) ) ) & ( ( for b8 being Element of b2 holds
( b8 _|_ b5 or b8 _|_ b3 ) ) implies ( b7 = PProJ b5,b6,b3,b4 iff b7 = 0. b1 ) ) );

theorem Th41: :: ORTSP_1:41
canceled;

theorem Th42: :: ORTSP_1:42
canceled;

theorem Th43: :: ORTSP_1:43
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 & b5 = 0. b2 holds
PProJ b4,b3,b5,b6 = 0. b1
proof end;

Lemma33: for b1 being Field
for b2 being OrtSp of b1
for b3 being Element of b2 holds b3 _|_ 0. b2
proof end;

theorem Th44: :: ORTSP_1:44
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 holds
( PProJ b4,b3,b5,b6 = 0. b1 iff b6 _|_ b5 )
proof end;

theorem Th45: :: ORTSP_1:45
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6 being Element of b2 st not b3 _|_ b4 holds
PProJ b4,b3,b5,b6 = PProJ b4,b3,b6,b5
proof end;

theorem Th46: :: ORTSP_1:46
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6 being Element of b2
for b7 being Element of b1 st not b3 _|_ b4 holds
PProJ b4,b3,b5,(b7 * b6) = b7 * (PProJ b4,b3,b5,b6)
proof end;

theorem Th47: :: ORTSP_1:47
for b1 being Field
for b2 being OrtSp of b1
for b3, b4, b5, b6, b7 being Element of b2 st not b3 _|_ b4 holds
PProJ b4,b3,b5,(b6 + b7) = (PProJ b4,b3,b5,b6) + (PProJ b4,b3,b5,b7)
proof end;