begin
deffunc H1( 1-sorted ) -> set = the carrier of $1;
deffunc H2( addLoopStr ) -> Element of bool [:[:the carrier of $1,the carrier of $1:],the carrier of $1:] = the addF of $1;
deffunc H3( non empty addLoopStr ) -> Element of bool [:the carrier of $1,the carrier of $1:] = comp $1;
deffunc H4( addLoopStr ) -> Element of the carrier of $1 = 0. $1;
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem Th4:
Lm1:
for G being non empty right_complementable Abelian add-associative right_zeroed addLoopStr holds comp G is_an_inverseOp_wrt the addF of G
theorem
Lm2:
for GS being non empty addLoopStr st the addF of GS is commutative & the addF of GS is associative holds
( GS is Abelian & GS is add-associative )
Lm3:
for GS being non empty addLoopStr st 0. GS is_a_unity_wrt the addF of GS holds
GS is right_zeroed
Lm4:
for F being Field holds the multF of F is associative
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th11:
Lm5:
for F being Field holds the multF of F is_distributive_wrt the addF of F
begin
definition
let D be non
empty set ;
let F be
BinOp of
D;
let n be
Nat;
func product F,
n -> BinOp of
(n -tuples_on D) means :
Def1:
for
x,
y being
Element of
n -tuples_on D holds
it . x,
y = F .: x,
y;
existence
ex b1 being BinOp of (n -tuples_on D) st
for x, y being Element of n -tuples_on D holds b1 . x,y = F .: x,y
uniqueness
for b1, b2 being BinOp of (n -tuples_on D) st ( for x, y being Element of n -tuples_on D holds b1 . x,y = F .: x,y ) & ( for x, y being Element of n -tuples_on D holds b2 . x,y = F .: x,y ) holds
b1 = b2
end;
:: deftheorem Def1 defines product PRVECT_1:def 1 :
:: deftheorem Def2 defines product PRVECT_1:def 2 :
theorem
canceled;
theorem
canceled;
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
begin
:: deftheorem Def3 defines -Group_over PRVECT_1:def 3 :
definition
let F be
Field;
let n be
Nat;
func n -Mult_over F -> Function of
[:the carrier of F,(n -tuples_on the carrier of F):],
(n -tuples_on the carrier of F) means :
Def4:
for
x being
Element of
F for
v being
Element of
n -tuples_on the
carrier of
F holds
it . x,
v = the
multF of
F [;] x,
v;
existence
ex b1 being Function of [:the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) st
for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b1 . x,v = the multF of F [;] x,v
uniqueness
for b1, b2 being Function of [:the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) st ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b1 . x,v = the multF of F [;] x,v ) & ( for x being Element of F
for v being Element of n -tuples_on the carrier of F holds b2 . x,v = the multF of F [;] x,v ) holds
b1 = b2
end;
:: deftheorem Def4 defines -Mult_over PRVECT_1:def 4 :
:: deftheorem Def5 defines -VectSp_over PRVECT_1:def 5 :
theorem Th18:
begin
begin
:: deftheorem PRVECT_1:def 6 :
canceled;
:: deftheorem PRVECT_1:def 7 :
canceled;
:: deftheorem Def8 defines BinOps PRVECT_1:def 8 :
:: deftheorem Def9 defines UnOps PRVECT_1:def 9 :
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
theorem Th24:
definition
let a be
Domain-Sequence;
let b be
BinOps of
a;
func [:b:] -> BinOp of
(product a) means :
Def10:
for
f,
g being
Element of
product a for
i being
Element of
dom a holds
(it . f,g) . i = (b . i) . (f . i),
(g . i);
existence
ex b1 being BinOp of (product a) st
for f, g being Element of product a
for i being Element of dom a holds (b1 . f,g) . i = (b . i) . (f . i),(g . i)
uniqueness
for b1, b2 being BinOp of (product a) st ( for f, g being Element of product a
for i being Element of dom a holds (b1 . f,g) . i = (b . i) . (f . i),(g . i) ) & ( for f, g being Element of product a
for i being Element of dom a holds (b2 . f,g) . i = (b . i) . (f . i),(g . i) ) holds
b1 = b2
end;
:: deftheorem Def10 defines [: PRVECT_1:def 10 :
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
begin
:: deftheorem Def11 defines AbGroup-yielding PRVECT_1:def 11 :
:: deftheorem Def12 defines carr PRVECT_1:def 12 :
:: deftheorem Def13 defines addop PRVECT_1:def 13 :
:: deftheorem Def14 defines complop PRVECT_1:def 14 :
:: deftheorem Def15 defines zeros PRVECT_1:def 15 :
:: deftheorem defines product PRVECT_1:def 16 :