let R be non degenerated comRing; :: thesis: for n being Nat
for x, y being Element of R
for D being Derivation of R holds LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>
let n be Nat; :: thesis: for x, y being Element of R
for D being Derivation of R holds LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>
let x, y be Element of R; :: thesis: for D being Derivation of R holds LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>
let D be Derivation of R; :: thesis: LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>
set p = LBZ (D,(n + 1),x,y);
set q = LBZ0 (D,n,x,y);
set r = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>;
set r1 = <*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y));
set r2 = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>;
set r3 = (LBZ0 (D,n,x,y)) ^ <*(x * ((D |^ (n + 1)) . y))*>;
<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y)) = Ins ((LBZ0 (D,n,x,y)),0,(((D |^ (n + 1)) . x) * y)) by FINSEQ_5:67;
then A2: len (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) = (len (LBZ0 (D,n,x,y))) + 1 by FINSEQ_5:69
.= n + 1 by Def5 ;
A3: len (LBZ (D,(n + 1),x,y)) = (n + 1) + 1 by Def4
.= n + 2 ;
(<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*> = Ins ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))),(n + 1),(x * ((D |^ (n + 1)) . y))) by A2, FINSEQ_5:68;
then A4: len ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) = (n + 1) + 1 by A2, FINSEQ_5:69
.= len (LBZ (D,(n + 1),x,y)) by A3 ;
for k being Nat st 1 <= k & k <= len (LBZ (D,(n + 1),x,y)) holds
(LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (LBZ (D,(n + 1),x,y)) implies (LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k )
assume A5: ( 1 <= k & k <= len (LBZ (D,(n + 1),x,y)) ) ; :: thesis: (LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k
A6: k in dom (LBZ (D,(n + 1),x,y)) by A5, FINSEQ_3:25;
(n + 1) + 1 > 0 + 1 by XREAL_1:8;
then A7: (n + 2) -' 1 = (n + 2) - 1 by XREAL_1:233
.= n + 1 ;
( 1 < k + 1 & k < (n + 2) + 1 ) by A5, A3, NAT_1:13;

per cases then ( k = 1 or ( 1 < k & k < n + 2 ) or k = n + 2 ) by NAT_1:22;

suppose A9: k = 1 ; :: thesis: (LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k

(n + 1) + 1 > 0 + 1 by XREAL_1:8;
then A10: (n + 2) -' 1 = (n + 2) - 1 by XREAL_1:233
.= n + 1 ;
A11: (LBZ (D,(n + 1),x,y)) . k = (((n + 1) choose (k -' 1)) * ((D |^ (((n + 1) + 1) -' k)) . x)) * ((D |^ (k -' 1)) . y) by A6, Def4
.= (((n + 1) choose 0) * ((D |^ ((n + 2) -' 1)) . x)) * ((D |^ (1 -' 1)) . y) by A9, XREAL_1:232
.= (1 * ((D |^ ((n + 2) -' 1)) . x)) * ((D |^ (1 -' 1)) . y) by NEWTON:19
.= ((D |^ ((n + 2) -' 1)) . x) * ((D |^ (1 -' 1)) . y) by BINOM:13
.= ((D |^ (n + 1)) . x) * ((D |^ 0) . y) by A10, XREAL_1:232
.= ((D |^ (n + 1)) . x) * ((id R) . y) by VECTSP11:18
.= ((D |^ (n + 1)) . x) * y ;
((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k = (Ins ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))),(n + 1),(x * ((D |^ (n + 1)) . y)))) . 1 by A9, A2, FINSEQ_5:68
.= (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) . 1 by NAT_1:11, FINSEQ_5:75
.= (LBZ (D,(n + 1),x,y)) . k by A11, FINSEQ_1:41 ;
hence (LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k ; :: thesis: verum

end;

suppose A12: ( 1 < k & k < n + 2 ) ; :: thesis: (LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k

A13: dom (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) = Seg (n + 1) by A2, FINSEQ_1:def 3;
1 + 1 <= k by A12, INT_1:7;
then A15: 2 - 1 <= k - 1 by XREAL_1:9;
k + 1 <= n + 2 by A12, INT_1:7;
then A17: (k + 1) - 1 <= (n + 2) - 1 by XREAL_1:9;
then A18: k in dom (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) by A13, A12;
reconsider s = k - 1 as Nat by A12;
reconsider q1 = <*(((D |^ (n + 1)) . x) * y)*> as FinSequence of R ;
A19: dom (LBZ0 (D,n,x,y)) = Seg (len (LBZ0 (D,n,x,y))) by FINSEQ_1:def 3
.= Seg n by Def5 ;
k - 1 <= (n + 1) - 1 by A17, XREAL_1:9;
then A21: s in dom (LBZ0 (D,n,x,y)) by A19, A15;
reconsider t = s - 1 as Nat by A15;
A22: k -' 1 = s by A12, XREAL_1:233;
A23: ((n + 1) + 1) -' k = ((n + 1) + 1) - k by A12, XREAL_1:233
.= (n + 1) - s
.= (n + 1) -' s by A12, A17, XREAL_1:9, XREAL_1:233 ;
((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k = (q1 ^ (LBZ0 (D,n,x,y))) . (s + 1) by A18, FINSEQ_1:def 7
.= (q1 ^ (LBZ0 (D,n,x,y))) . ((len q1) + s) by FINSEQ_1:39
.= (LBZ0 (D,n,x,y)) . s by A21, FINSEQ_1:def 7
.= (((n choose (s -' 1)) + (n choose s)) * ((D |^ ((n + 1) -' s)) . x)) * ((D |^ s) . y) by A21, Def5
.= (((n choose t) + (n choose (t + 1))) * ((D |^ ((n + 1) -' s)) . x)) * ((D |^ s) . y) by A15, XREAL_1:233
.= (((n + 1) choose (k -' 1)) * ((D |^ (((n + 1) + 1) -' k)) . x)) * ((D |^ (k -' 1)) . y) by A23, A22, NEWTON:22
.= (LBZ (D,(n + 1),x,y)) . k by A6, Def4 ;
hence (LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k ; :: thesis: verum

end;

suppose A24: k = n + 2 ; :: thesis: (LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k

then A25: ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k = (Ins ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))),(n + 1),(x * ((D |^ (n + 1)) . y)))) . ((n + 1) + 1) by A2, FINSEQ_5:68
.= x * ((D |^ (n + 1)) . y) by FINSEQ_5:73, A2 ;
(LBZ (D,(n + 1),x,y)) . k = (((n + 1) choose (n + 1)) * ((D |^ (((n + 1) + 1) -' (n + 2))) . x)) * ((D |^ ((n + 2) -' 1)) . y) by A7, A24, A6, Def4
.= (1 * ((D |^ (((n + 1) + 1) -' (n + 2))) . x)) * ((D |^ ((n + 2) -' 1)) . y) by NEWTON:21
.= ((D |^ ((n + 2) -' (n + 2))) . x) * ((D |^ ((n + 2) -' 1)) . y) by BINOM:13
.= ((D |^ 0) . x) * ((D |^ (n + 1)) . y) by A7, XREAL_1:232
.= ((id R) . x) * ((D |^ (n + 1)) . y) by VECTSP11:18
.= ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k by A25 ;
hence (LBZ (D,(n + 1),x,y)) . k = ((<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*>) . k ; :: thesis: verum

end;

end;

end;

hence LBZ (D,(n + 1),x,y) = (<*(((D |^ (n + 1)) . x) * y)*> ^ (LBZ0 (D,n,x,y))) ^ <*(x * ((D |^ (n + 1)) . y))*> by A4; :: thesis: verum