let a, b, c, d be Real; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: (((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; :: thesis: verum