let R be non degenerated comRing; for n being Nat
for x, y being Element of R
for D being Derivation of R holds D * (LBZ0 (D,n,x,y)) = (Del ((LBZ2 (D,(n + 1),x,y)),(n + 1))) + (Del ((LBZ1 (D,(n + 1),x,y)),1))
let n be Nat; for x, y being Element of R
for D being Derivation of R holds D * (LBZ0 (D,n,x,y)) = (Del ((LBZ2 (D,(n + 1),x,y)),(n + 1))) + (Del ((LBZ1 (D,(n + 1),x,y)),1))
let x, y be Element of R; for D being Derivation of R holds D * (LBZ0 (D,n,x,y)) = (Del ((LBZ2 (D,(n + 1),x,y)),(n + 1))) + (Del ((LBZ1 (D,(n + 1),x,y)),1))
let D be Derivation of R; D * (LBZ0 (D,n,x,y)) = (Del ((LBZ2 (D,(n + 1),x,y)),(n + 1))) + (Del ((LBZ1 (D,(n + 1),x,y)),1))
set p = LBZ2 (D,(n + 1),x,y);
set q = LBZ1 (D,(n + 1),x,y);
set r = LBZ0 (D,n,x,y);
A1:
len (LBZ2 (D,(n + 1),x,y)) = n + 1
by Def7;
A2:
len (LBZ1 (D,(n + 1),x,y)) = n + 1
by Def6;
A3: dom (LBZ2 (D,(n + 1),x,y)) =
Seg (len (LBZ2 (D,(n + 1),x,y)))
by FINSEQ_1:def 3
.=
Seg (n + 1)
by Def7
;
A4: dom (LBZ1 (D,(n + 1),x,y)) =
Seg (len (LBZ1 (D,(n + 1),x,y)))
by FINSEQ_1:def 3
.=
Seg (n + 1)
by Def6
;
A5: dom (LBZ0 (D,n,x,y)) =
Seg (len (LBZ0 (D,n,x,y)))
by FINSEQ_1:def 3
.=
Seg n
by Def5
;
A6:
1 <= n + 1
by NAT_1:12;
then A7:
n + 1 in dom (LBZ2 (D,(n + 1),x,y))
by A1, FINSEQ_3:25;
A8:
1 in dom (LBZ1 (D,(n + 1),x,y))
by A2, A6, FINSEQ_3:25;
reconsider p1 = Del ((LBZ2 (D,(n + 1),x,y)),(n + 1)) as FinSequence of the carrier of R ;
reconsider q1 = Del ((LBZ1 (D,(n + 1),x,y)),1) as FinSequence of the carrier of R ;
A9: dom (Del ((LBZ2 (D,(n + 1),x,y)),(n + 1))) =
Seg (len p1)
by FINSEQ_1:def 3
.=
Seg n
by A1, FINSEQ_3:109, A7
;
A10: dom (Del ((LBZ1 (D,(n + 1),x,y)),1)) =
Seg (len q1)
by FINSEQ_1:def 3
.=
Seg n
by A2, FINSEQ_3:109, A8
;
A11:
dom (p1 + q1) = Seg n
by A9, BINOM:def 1;
A12: Seg (len (p1 + q1)) =
dom (p1 + q1)
by FINSEQ_1:def 3
.=
Seg n
by A9, BINOM:def 1
;
A14: len (D * (LBZ0 (D,n,x,y))) =
len (LBZ0 (D,n,x,y))
by FINSEQ_2:33
.=
n
by Def5
;
for i being Nat st 1 <= i & i <= len (D * (LBZ0 (D,n,x,y))) holds
(D * (LBZ0 (D,n,x,y))) . i = (p1 + q1) . i
proof
let i be
Nat;
( 1 <= i & i <= len (D * (LBZ0 (D,n,x,y))) implies (D * (LBZ0 (D,n,x,y))) . i = (p1 + q1) . i )
assume A16:
( 1
<= i &
i <= len (D * (LBZ0 (D,n,x,y))) )
;
(D * (LBZ0 (D,n,x,y))) . i = (p1 + q1) . i
then A17:
i in dom (LBZ0 (D,n,x,y))
by A5, A14;
A18:
i in dom (D * (LBZ0 (D,n,x,y)))
by A16, FINSEQ_3:25;
A19:
i in dom (p1 + q1)
by A14, A16, A11;
A20:
( 1
<= i &
i <= len (p1 + q1) )
by A12, FINSEQ_1:6, A14, A16;
A21:
i < n + 1
by A14, A16, XREAL_1:39;
A22:
( 1
<= i &
i <= n + 1 )
by A14, A16, XREAL_1:39;
then A23:
i in dom (LBZ2 (D,(n + 1),x,y))
by A3;
i in dom p1
by A14, A16, A9;
then A24:
p1 /. i =
p1 . i
by PARTFUN1:def 6
.=
(LBZ2 (D,(n + 1),x,y)) . i
by A21, FINSEQ_3:110
.=
(((n + 1) choose i) * ((D |^ (((n + 1) + 1) -' i)) . x)) * ((D |^ i) . y)
by A23, Def7
.=
(((n + 1) choose i) * ((D |^ ((n + 2) -' i)) . x)) * ((D |^ i) . y)
;
A25:
1
<= i + 1
by NAT_1:12;
A26:
i + 1
<= n + 1
by A21, INT_1:7;
then A28:
((n + 1) + 1) -' (i + 1) =
(n + 2) - (i + 1)
by XREAL_1:38, XREAL_1:233
.=
(n + 1) - i
.=
(n + 1) -' i
by A22, XREAL_1:233
;
A27:
i + 1
in dom (LBZ1 (D,(n + 1),x,y))
by A25, A26, A4;
A29:
i in dom q1
by A14, A16, A10;
A30:
1
in dom (LBZ1 (D,(n + 1),x,y))
by A4, A6;
reconsider qq1 =
q1 as the
carrier of
R -valued Function ;
reconsider ii =
i as
object ;
A31:
q1 /. i =
qq1 . ii
by A29, PARTFUN1:def 6
.=
(LBZ1 (D,(n + 1),x,y)) . (i + 1)
by A14, A16, A2, A30, FINSEQ_3:111
;
A32:
q1 /. i =
(((n + 1) choose ((i + 1) -' 1)) * ((D |^ (((n + 1) + 1) -' (i + 1))) . x)) * ((D |^ (i + 1)) . y)
by A27, A31, Def6
.=
(((n + 1) choose i) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ (i + 1)) . y)
by A28, NAT_D:34
;
A33:
i <= n + 2
by A14, A16, XREAL_1:39;
A34:
((n + 1) -' i) + 1 =
((n + 1) - i) + 1
by A22, XREAL_1:233
.=
(n + 2) - i
.=
(n + 2) -' i
by A33, XREAL_1:233
;
i in dom (LBZ0 (D,n,x,y))
by A14, A16, A5;
then A35:
(LBZ0 (D,n,x,y)) . i =
(((n choose i) + (n choose (i -' 1))) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ i) . y)
by Def5
.=
(((n choose ((i -' 1) + 1)) + (n choose (i -' 1))) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ i) . y)
by A16, XREAL_1:235
.=
(((n + 1) choose ((i -' 1) + 1)) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ i) . y)
by NEWTON:22
.=
(((n + 1) choose i) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ i) . y)
by A16, XREAL_1:235
;
(D * (LBZ0 (D,n,x,y))) /. i =
(D * (LBZ0 (D,n,x,y))) . i
by A18, PARTFUN1:def 6
.=
D . ((((n + 1) choose i) * ((D |^ ((n + 1) -' i)) . x)) * ((D |^ i) . y))
by A35, A17, FUNCT_1:13
.=
((D . (((n + 1) choose i) * ((D |^ ((n + 1) -' i)) . x))) * ((D |^ i) . y)) + ((((n + 1) choose i) * ((D |^ ((n + 1) -' i)) . x)) * (D . ((D |^ i) . y)))
by Def1
.=
((((n + 1) choose i) * (D . ((D |^ ((n + 1) -' i)) . x))) * ((D |^ i) . y)) + ((((n + 1) choose i) * ((D |^ ((n + 1) -' i)) . x)) * (D . ((D |^ i) . y)))
by Th6
.=
((((n + 1) choose i) * ((D |^ (((n + 1) -' i) + 1)) . x)) * ((D |^ i) . y)) + ((((n + 1) choose i) * ((D |^ ((n + 1) -' i)) . x)) * (D . ((D |^ i) . y)))
by Th9
.=
(p1 /. i) + (q1 /. i)
by A32, A24, A34, Th9
.=
(p1 + q1) /. i
by A20, BINOM:def 1
;
then (D * (LBZ0 (D,n,x,y))) . i =
(p1 + q1) /. i
by A18, PARTFUN1:def 6
.=
(p1 + q1) . i
by A19, PARTFUN1:def 6
;
hence
(D * (LBZ0 (D,n,x,y))) . i = (p1 + q1) . i
;
verum
end;
hence
D * (LBZ0 (D,n,x,y)) = (Del ((LBZ2 (D,(n + 1),x,y)),(n + 1))) + (Del ((LBZ1 (D,(n + 1),x,y)),1))
by A14, A12, FINSEQ_1:6; verum