let n be Nat; :: thesis: value ((<%1%> ^ (n --> 3)),10) = ((10 |^ (n + 1)) - 7) / 3
defpred S₁[ Nat] means 3 * (value ((<%1%> ^ ($1 --> 3)),10)) = (10 |^ ($1 + 1)) - 7;
value ((<%1%> ^ (0 --> 3)),10) = 1 by NUMBER11:2;
then A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set n1 = n + 1;
set N = <%1%> ^ (n --> 3);
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
(Segm (n + 1)) --> 3 = ((Segm n) --> 3) ^ <%3%> by AFINSQ_1:87;
then <%1%> ^ ((n + 1) --> 3) = (<%1%> ^ (n --> 3)) ^ <%3%> by AFINSQ_1:27;
then A4: value ((<%1%> ^ ((n + 1) --> 3)),10) = (value ((<%1%> ^ (n --> 3)),10)) + ((value (<%3%>,10)) * (10 |^ (len (<%1%> ^ (n --> 3))))) by Th1;
( len (n --> 3) = n & len <%1%> = 1 ) by AFINSQ_1:34;
then A5: len (<%1%> ^ (n --> 3)) = n + 1 by AFINSQ_1:17;
value (<%3%>,10) = 3 by NUMBER11:2;
then 3 * (value ((<%1%> ^ ((n + 1) --> 3)),10)) = (3 * (value ((<%1%> ^ (n --> 3)),10))) + (3 * (3 * (10 |^ (n + 1)))) by A5, A4;
then 3 * (value ((<%1%> ^ ((n + 1) --> 3)),10)) = ((1 + 9) * (10 |^ (n + 1))) - 7 by A3
.= (10 |^ ((n + 1) + 1)) - 7 by NEWTON:6 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A6: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
3 * (value ((<%1%> ^ (n --> 3)),10)) = (10 |^ (n + 1)) - 7 by A6;
hence value ((<%1%> ^ (n --> 3)),10) = ((10 |^ (n + 1)) - 7) / 3 ; :: thesis: verum