let X be BCI-algebra; :: thesis: for x, y being Element of X
for m, n being Nat holds Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x)

let x, y be Element of X; :: thesis: for m, n being Nat holds Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x)
let m, n be Nat; :: thesis: Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x)
consider f being sequence of the carrier of X such that
A1: (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power (n + 1) = f . (n + 1) and
A2: f . 0 = (x,(x \ y)) to_power (m + 1) and
A3: for k being Nat st k < n + 1 holds
f . (k + 1) = (f . k) \ (y \ x) by BCIALG_2:def 1;
consider g being sequence of the carrier of X such that
A4: (((x,(x \ y)) to_power (m + 1)),(y \ x)) to_power n = g . n and
A5: g . 0 = (x,(x \ y)) to_power (m + 1) and
A6: for k being Nat st k < n holds
g . (k + 1) = (g . k) \ (y \ x) by BCIALG_2:def 1;
defpred S1[ Nat] means ( \$1 <= n implies f . \$1 = g . \$1 );
now :: thesis: for k being Nat st ( k <= n implies f . k = g . k ) & k + 1 <= n holds
f . (k + 1) = g . (k + 1)
let k be Nat; :: thesis: ( ( k <= n implies f . k = g . k ) & k + 1 <= n implies f . (k + 1) = g . (k + 1) )
assume A7: ( k <= n implies f . k = g . k ) ; :: thesis: ( k + 1 <= n implies f . (k + 1) = g . (k + 1) )
set m = k + 1;
assume A8: k + 1 <= n ; :: thesis: f . (k + 1) = g . (k + 1)
then k + 1 <= n + 1 by NAT_1:13;
then k < n + 1 by NAT_1:13;
then A9: f . (k + 1) = (f . k) \ (y \ x) by A3;
k < n by ;
hence f . (k + 1) = g . (k + 1) by A6, A7, A9; :: thesis: verum
end;
then A10: for k being Nat st S1[k] holds
S1[k + 1] ;
A11: S1[ 0 ] by A2, A5;
for n being Nat holds S1[n] from then f . n = g . n ;
hence Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x) by ; :: thesis: verum