begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem
canceled;
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem defines multfield FVSUM_1:def 1 :
for K being non empty multMagma
for a being Element of K holds a multfield = the multF of K [;] (a,(id the carrier of K));
:: deftheorem defines diffield FVSUM_1:def 2 :
for K being non empty addLoopStr holds diffield K = the addF of K * ((id the carrier of K),(comp K));
theorem
canceled;
theorem Th14:
Lm1:
for K being non empty multMagma
for a, b being Element of K holds ( the multF of K [;] (b,(id the carrier of K))) . a = b * a
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
begin
:: deftheorem defines + FVSUM_1:def 3 :
for K being non empty addLoopStr
for p1, p2 being FinSequence of the carrier of K holds p1 + p2 = the addF of K .: (p1,p2);
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem
Lm2:
for i being Element of NAT
for K being non empty left_zeroed right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R
theorem
canceled;
theorem
canceled;
theorem Th28:
:: deftheorem defines - FVSUM_1:def 4 :
for K being non empty addLoopStr
for p being FinSequence of the carrier of K holds - p = (comp K) * p;
theorem
canceled;
theorem Th30:
theorem
theorem
canceled;
theorem
theorem Th34:
Lm3:
for i being Element of NAT
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K)
theorem Th35:
theorem Th36:
theorem Th37:
theorem
Lm4:
for i being Element of NAT
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds
R1 = R2
theorem
theorem Th40:
:: deftheorem defines - FVSUM_1:def 5 :
for K being non empty addLoopStr
for p1, p2 being FinSequence of the carrier of K holds p1 - p2 = (diffield K) .: (p1,p2);
theorem
canceled;
theorem Th42:
theorem
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem Th52:
theorem Th53:
theorem
theorem
theorem Th56:
theorem
theorem
theorem
theorem Th60:
theorem
:: deftheorem defines * FVSUM_1:def 6 :
for K being non empty multMagma
for p being FinSequence of the carrier of K
for a being Element of K holds a * p = (a multfield) * p;
theorem Th62:
theorem
theorem
canceled;
theorem
theorem Th66:
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines mlt FVSUM_1:def 7 :
for M being non empty multMagma
for p1, p2 being FinSequence of the carrier of M holds mlt (p1,p2) = the multF of M .: (p1,p2);
theorem
theorem
theorem
canceled;
theorem
Lm5:
for K being non empty multMagma
for a1, a2, b1, b2 being Element of K holds mlt (<*a1,a2*>,<*b1,b2*>) = <*(a1 * b1),(a2 * b2)*>
theorem
theorem Th78:
theorem
theorem Th80:
theorem
theorem
theorem
theorem
begin
:: deftheorem defines Sum FVSUM_1:def 8 :
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of K holds Sum p = the addF of K $$ p;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
begin
Lm6:
for K being non empty commutative well-unital multLoopStr holds Product (<*> the carrier of K) = 1. K
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th111:
theorem
begin
:: deftheorem FVSUM_1:def 9 :
canceled;
:: deftheorem defines "*" FVSUM_1:def 10 :
for K being non empty doubleLoopStr
for p, q being FinSequence of the carrier of K holds p "*" q = Sum (mlt (p,q));
theorem
theorem
theorem