let a, b be Real; :: thesis: for n being Nat holds
( len ((a,b) In_Power n) = len (Newton_Coeff n) & len ((a,b) Subnomial n) = len (Newton_Coeff n) & len ((a,b) In_Power n) = len ((a,b) Subnomial n) & dom ((a,b) In_Power n) = dom (Newton_Coeff n) & dom ((a,b) Subnomial n) = dom (Newton_Coeff n) & dom ((a,b) In_Power n) = dom ((a,b) Subnomial n) )
let n be Nat; :: thesis: ( len ((a,b) In_Power n) = len (Newton_Coeff n) & len ((a,b) Subnomial n) = len (Newton_Coeff n) & len ((a,b) In_Power n) = len ((a,b) Subnomial n) & dom ((a,b) In_Power n) = dom (Newton_Coeff n) & dom ((a,b) Subnomial n) = dom (Newton_Coeff n) & dom ((a,b) In_Power n) = dom ((a,b) Subnomial n) )
len ((a,b) In_Power ((n + 1) - 1)) = len (Newton_Coeff n) ;
then A2: dom ((a,b) In_Power n) = dom (Newton_Coeff n) by FINSEQ_3:29;
dom (((a,b) In_Power n) /" (Newton_Coeff n)) = (dom ((a,b) In_Power n)) /\ (dom (Newton_Coeff n)) by VALUED_1:16;
hence ( len ((a,b) In_Power n) = len (Newton_Coeff n) & len ((a,b) Subnomial n) = len (Newton_Coeff n) & len ((a,b) In_Power n) = len ((a,b) Subnomial n) & dom ((a,b) In_Power n) = dom (Newton_Coeff n) & dom ((a,b) Subnomial n) = dom (Newton_Coeff n) & dom ((a,b) In_Power n) = dom ((a,b) Subnomial n) ) by A2, FINSEQ_3:29; :: thesis: verum