begin
theorem Th1:
theorem Th2:
begin
theorem Th3:
theorem
theorem Th5:
theorem
:: deftheorem BINOM:def 1 :
canceled;
:: deftheorem BINOM:def 2 :
canceled;
:: deftheorem BINOM:def 3 :
canceled;
:: deftheorem Def4 defines + BINOM:def 4 :
theorem Th7:
begin
:: deftheorem defines |^ BINOM:def 5 :
theorem Th8:
theorem
canceled;
theorem
theorem Th11:
theorem
begin
definition
let R be non
empty addLoopStr ;
func Nat-mult-left R -> Function of
[:NAT ,the carrier of R:],the
carrier of
R means :
Def6:
for
a being
Element of holds
(
it . 0 ,
a = 0. R & ( for
n being
Element of
NAT holds
it . (n + 1),
a = a + (it . n,a) ) );
existence
ex b1 being Function of [:NAT ,the carrier of R:],the carrier of R st
for a being Element of holds
( b1 . 0 ,a = 0. R & ( for n being Element of NAT holds b1 . (n + 1),a = a + (b1 . n,a) ) )
uniqueness
for b1, b2 being Function of [:NAT ,the carrier of R:],the carrier of R st ( for a being Element of holds
( b1 . 0 ,a = 0. R & ( for n being Element of NAT holds b1 . (n + 1),a = a + (b1 . n,a) ) ) ) & ( for a being Element of holds
( b2 . 0 ,a = 0. R & ( for n being Element of NAT holds b2 . (n + 1),a = a + (b2 . n,a) ) ) ) holds
b1 = b2
func Nat-mult-right R -> Function of
[:the carrier of R,NAT :],the
carrier of
R means :
Def7:
for
a being
Element of holds
(
it . a,
0 = 0. R & ( for
n being
Element of
NAT holds
it . a,
(n + 1) = (it . a,n) + a ) );
existence
ex b1 being Function of [:the carrier of R,NAT :],the carrier of R st
for a being Element of holds
( b1 . a,0 = 0. R & ( for n being Element of NAT holds b1 . a,(n + 1) = (b1 . a,n) + a ) )
uniqueness
for b1, b2 being Function of [:the carrier of R,NAT :],the carrier of R st ( for a being Element of holds
( b1 . a,0 = 0. R & ( for n being Element of NAT holds b1 . a,(n + 1) = (b1 . a,n) + a ) ) ) & ( for a being Element of holds
( b2 . a,0 = 0. R & ( for n being Element of NAT holds b2 . a,(n + 1) = (b2 . a,n) + a ) ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines Nat-mult-left BINOM:def 6 :
:: deftheorem Def7 defines Nat-mult-right BINOM:def 7 :
:: deftheorem defines * BINOM:def 8 :
:: deftheorem defines * BINOM:def 9 :
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem Th22:
begin
definition
let R be non
empty unital doubleLoopStr ;
let a,
b be
Element of ;
let n be
Element of
NAT ;
func a,
b In_Power n -> FinSequence of the
carrier of
R means :
Def10:
(
len it = n + 1 & ( for
i,
l,
m being
Element of
NAT st
i in dom it &
m = i - 1 &
l = n - m holds
it /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) );
existence
ex b1 being FinSequence of the carrier of R st
( len b1 = n + 1 & ( for i, l, m being Element of NAT st i in dom b1 & m = i - 1 & l = n - m holds
b1 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) )
uniqueness
for b1, b2 being FinSequence of the carrier of R st len b1 = n + 1 & ( for i, l, m being Element of NAT st i in dom b1 & m = i - 1 & l = n - m holds
b1 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len b2 = n + 1 & ( for i, l, m being Element of NAT st i in dom b2 & m = i - 1 & l = n - m holds
b2 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) holds
b1 = b2
end;
:: deftheorem Def10 defines In_Power BINOM:def 10 :
theorem Th23:
theorem Th24:
theorem Th25:
theorem