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_{1}[ Nat] means ( $1 <= n implies f . $1 = g . $1 );

_{1}[k] holds

S_{1}[k + 1]
;

A11: S_{1}[ 0 ]
by A2, A5;

for n being Nat holds S_{1}[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

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

now :: thesis: for k being Nat st ( k <= n implies f . k = g . k ) & k + 1 <= n holds

f . (k + 1) = g . (k + 1)

then A10:
for k being Nat st Sf . (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;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

S

A11: S

for n being Nat holds S

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