let a, b, c, d be Real; for n being Nat
for x being object st x in dom (((a * b),(c * d)) Subnomial n) holds
(((a * b),(c * d)) Subnomial n) . x = (((a,d) Subnomial n) . x) * (((b,c) Subnomial n) . x)
let n be Nat; for x being object st x in dom (((a * b),(c * d)) Subnomial n) holds
(((a * b),(c * d)) Subnomial n) . x = (((a,d) Subnomial n) . x) * (((b,c) Subnomial n) . x)
let x be object ; ( x in dom (((a * b),(c * d)) Subnomial n) implies (((a * b),(c * d)) Subnomial n) . x = (((a,d) Subnomial n) . x) * (((b,c) Subnomial n) . x) )
assume B1:
x in dom (((a * b),(c * d)) Subnomial n)
; (((a * b),(c * d)) Subnomial n) . x = (((a,d) Subnomial n) . x) * (((b,c) Subnomial n) . x)
( len (((a * b),(c * d)) Subnomial ((n + 1) - 1)) = len ((a,d) Subnomial ((n + 1) - 1)) & len (((a * b),(c * d)) Subnomial ((n + 1) - 1)) = len ((b,c) Subnomial ((n + 1) - 1)) )
;
then A0:
( dom (((a * b),(c * d)) Subnomial n) = dom ((a,d) Subnomial n) & dom (((a * b),(c * d)) Subnomial n) = dom ((b,c) Subnomial n) )
by FINSEQ_3:29;
reconsider x = x as positive Nat by B1, FINSEQ_3:25;
set m = x - 1;
len (((a * b),(c * d)) Subnomial ((n + 1) - 1)) >= x
by B1, FINSEQ_3:25;
then consider k being Nat such that
B2:
n + 1 = x + k
by NAT_1:10;
B3:
( n = (x - 1) + k & k = n - (x - 1) )
by B2;
then (((a * b),(c * d)) Subnomial ((x - 1) + k)) . ((x - 1) + 1) =
((a * b) |^ k) * ((c * d) |^ (x - 1))
by B1, Def2
.=
((a |^ k) * (b |^ k)) * ((c * d) |^ (x - 1))
by NEWTON:7
.=
((a |^ k) * (b |^ k)) * ((c |^ (x - 1)) * (d |^ (x - 1)))
by NEWTON:7
.=
((a |^ k) * (d |^ (x - 1))) * ((b |^ k) * (c |^ (x - 1)))
.=
(((a,d) Subnomial ((x - 1) + k)) . ((x - 1) + 1)) * ((b |^ k) * (c |^ (x - 1)))
by A0, B1, B3, Def2
.=
(((a,d) Subnomial ((x - 1) + k)) . ((x - 1) + 1)) * (((b,c) Subnomial ((x - 1) + k)) . ((x - 1) + 1))
by A0, B1, B3, Def2
;
hence
(((a * b),(c * d)) Subnomial n) . x = (((a,d) Subnomial n) . x) * (((b,c) Subnomial n) . x)
by B2; verum