let R be non degenerated comRing; for m being Nat
for x, y being Element of R
for D being Derivation of R holds LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))
let m be Nat; for x, y being Element of R
for D being Derivation of R holds LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))
let x, y be Element of R; for D being Derivation of R holds LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))
let D be Derivation of R; LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))
set p = LBZ1 (D,m,x,y);
set q = LBZ2 (D,m,x,y);
set r = LBZ0 (D,m,x,y);
A1: dom (LBZ1 (D,m,x,y)) =
Seg (len (LBZ1 (D,m,x,y)))
by FINSEQ_1:def 3
.=
Seg m
by Def6
;
A2: dom (LBZ2 (D,m,x,y)) =
Seg (len (LBZ2 (D,m,x,y)))
by FINSEQ_1:def 3
.=
Seg m
by Def7
;
A3: dom (LBZ0 (D,m,x,y)) =
Seg (len (LBZ0 (D,m,x,y)))
by FINSEQ_1:def 3
.=
Seg m
by Def5
;
A4:
dom ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) = Seg m
by A1, BINOM:def 1;
A5: Seg (len ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y)))) =
dom ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y)))
by FINSEQ_1:def 3
.=
dom (LBZ1 (D,m,x,y))
by BINOM:def 1
.=
Seg (len (LBZ1 (D,m,x,y)))
by FINSEQ_1:def 3
.=
Seg m
by Def6
;
A6: len (LBZ0 (D,m,x,y)) =
m
by Def5
.=
len ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y)))
by A5, FINSEQ_1:6
;
for k being Nat st 1 <= k & k <= len ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) holds
((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) . k = (LBZ0 (D,m,x,y)) . k
proof
let k be
Nat;
( 1 <= k & k <= len ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) implies ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) . k = (LBZ0 (D,m,x,y)) . k )
assume A7:
( 1
<= k &
k <= len ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) )
;
((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) . k = (LBZ0 (D,m,x,y)) . k
then A8:
k in dom (LBZ1 (D,m,x,y))
by A1, A5;
then A9:
(LBZ1 (D,m,x,y)) /. k =
(LBZ1 (D,m,x,y)) . k
by PARTFUN1:def 6
.=
((m choose (k -' 1)) * ((D |^ ((m + 1) -' k)) . x)) * ((D |^ k) . y)
by A8, Def6
;
A10:
k in dom (LBZ2 (D,m,x,y))
by A2, A5, A7;
then A11:
(LBZ2 (D,m,x,y)) /. k =
(LBZ2 (D,m,x,y)) . k
by PARTFUN1:def 6
.=
((m choose k) * ((D |^ ((m + 1) -' k)) . x)) * ((D |^ k) . y)
by A10, Def7
;
A12:
k in dom (LBZ0 (D,m,x,y))
by A3, A5, A7;
k in dom ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y)))
by A4, A5, A7;
then ((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) . k =
((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) /. k
by PARTFUN1:def 6
.=
(((m choose (k -' 1)) * ((D |^ ((m + 1) -' k)) . x)) * ((D |^ k) . y)) + (((m choose k) * ((D |^ ((m + 1) -' k)) . x)) * ((D |^ k) . y))
by A11, A9, A7, BINOM:def 1
.=
((m choose (k -' 1)) * (((D |^ ((m + 1) -' k)) . x) * ((D |^ k) . y))) + (((m choose k) * ((D |^ ((m + 1) -' k)) . x)) * ((D |^ k) . y))
by BINOM:19
.=
((m choose (k -' 1)) * (((D |^ ((m + 1) -' k)) . x) * ((D |^ k) . y))) + ((m choose k) * (((D |^ ((m + 1) -' k)) . x) * ((D |^ k) . y)))
by BINOM:19
.=
((m choose (k -' 1)) + (m choose k)) * (((D |^ ((m + 1) -' k)) . x) * ((D |^ k) . y))
by BINOM:15
.=
(((m choose (k -' 1)) + (m choose k)) * ((D |^ ((m + 1) -' k)) . x)) * ((D |^ k) . y)
by BINOM:19
.=
(LBZ0 (D,m,x,y)) . k
by A12, Def5
;
hence
((LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))) . k = (LBZ0 (D,m,x,y)) . k
;
verum
end;
hence
LBZ0 (D,m,x,y) = (LBZ1 (D,m,x,y)) + (LBZ2 (D,m,x,y))
by A6; verum