let n be Nat; :: thesis: for a being Real holds (a,a) Subnomial n = (n + 1) |-> (a |^ n)
let a be Real; :: thesis: (a,a) Subnomial n = (n + 1) |-> (a |^ n)
A1: for j being Nat holds ((a,a) Subnomial n) . j = ((n + 1) |-> (a |^ n)) . j

proof

let j be Nat; :: thesis: ((a,a) Subnomial n) . j = ((n + 1) |-> (a |^ n)) . j
( j <> 0 implies ((a,a) Subnomial n) . j = ((n + 1) |-> (a |^ n)) . j )

proof

assume j <> 0 ; :: thesis: ((a,a) Subnomial n) . j = ((n + 1) |-> (a |^ n)) . j
then reconsider i = j - 1 as Nat ;

per cases ( ex k being Nat st n = i + k or for k being Nat holds not n = i + k ) ;

suppose ex k being Nat st n = i + k ; :: thesis: ((a,a) Subnomial n) . j = ((n + 1) |-> (a |^ n)) . j

then reconsider k = n - i as Nat ;
set l = i + 1;
( 0 + 1 <= i + 1 & (i + 1) + 0 <= (i + 1) + k ) by XREAL_1:6;
then ( 1 <= i + 1 & i + 1 <= len ((a,a) Subnomial ((n + 1) - 1)) ) ;
then i + 1 in dom ((a,a) Subnomial (i + k)) by FINSEQ_3:25;
then ( ((a,a) Subnomial (i + k)) . (i + 1) = a |^ n & ((k + (i + 1)) |-> (a |^ n)) . (i + 1) = a |^ n ) by CONST;
hence ((a,a) Subnomial n) . j = ((n + 1) |-> (a |^ n)) . j ; :: thesis: verum

end;

suppose for k being Nat holds not n = i + k ; :: thesis: ((a,a) Subnomial n) . j = ((n + 1) |-> (a |^ n)) . j

then i + 1 > n + 1 by XREAL_1:6, NAT_1:10;
then ( i + 1 > len ((a,a) Subnomial n) & i + 1 > len ((n + 1) |-> (a |^ n)) & len ((n + 1) |-> (a |^ n)) = n + 1 ) by Def2;
then ( not i + 1 in dom ((a,a) Subnomial n) & not i + 1 in dom ((n + 1) |-> (a |^ n)) ) by FINSEQ_3:25;
then ( ((a,a) Subnomial n) . (i + 1) = 0 & ((n + 1) |-> (a |^ n)) . (i + 1) = 0 ) by FUNCT_1:def 2;
hence ((a,a) Subnomial n) . j = ((n + 1) |-> (a |^ n)) . j ; :: thesis: verum

end;

end;

end;

hence ((a,a) Subnomial n) . j = ((n + 1) |-> (a |^ n)) . j ; :: thesis: verum

end;

len ((a,a) Subnomial ((n + 1) - 1)) = len ((n + 1) |-> (a |^ n)) ;
hence (a,a) Subnomial n = (n + 1) |-> (a |^ n) by A1; :: thesis: verum