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 S₁[ 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 A8, NAT_1:13;
hence f . (k + 1) = g . (k + 1) by A6, A7, A9; :: thesis: verum

end;

then A10: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A11: S₁[ 0 ] by A2, A5;
for n being Nat holds S₁[n] from NAT_1:sch 2(A11, A10);
then f . n = g . n ;
hence Polynom (m,(n + 1),x,y) = (Polynom (m,n,x,y)) \ (y \ x) by A1, A3, A4, XREAL_1:29; :: thesis: verum