let X be BCI-algebra; :: thesis: for x, y being Element of X
for m, n being Element of 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 Element of NAT holds Polynom m,(n + 1),x,y = (Polynom m,n,x,y) \ (y \ x)
let m, n be Element of NAT ; :: thesis: Polynom m,(n + 1),x,y = (Polynom m,n,x,y) \ (y \ x)
consider f being Function of NAT ,the carrier of X such that
A1: ( (x,(x \ y) to_power (m + 1)),(y \ x) to_power (n + 1) = f . (n + 1) & f . 0 = x,(x \ y) to_power (m + 1) & ( for k being Element of NAT st k < n + 1 holds
f . (k + 1) = (f . k) \ (y \ x) ) ) by BCIALG_2:def 1;
consider g being Function of NAT ,the carrier of X such that
A2: ( (x,(x \ y) to_power (m + 1)),(y \ x) to_power n = g . n & g . 0 = x,(x \ y) to_power (m + 1) & ( for k being Element of NAT st k < n holds
g . (k + 1) = (g . k) \ (y \ x) ) ) by BCIALG_2:def 1;
defpred S₁[ Element of NAT ] means ( $1 <= n implies f . $1 = g . $1 );
A3: S₁[ 0 ] by A1, A2;
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

now

let k be Element of NAT ; :: thesis: ( ( k <= n implies f . k = g . k ) & k + 1 <= n implies f . (k + 1) = g . (k + 1) )
assume A5: ( k <= n implies f . k = g . k ) ; :: thesis: ( k + 1 <= n implies f . (k + 1) = g . (k + 1) )
set m = k + 1;
assume A6: k + 1 <= n ; :: thesis: f . (k + 1) = g . (k + 1)
A7: ( k < n + 1 & k < n & k <= n )

proof

k + 1 <= n + 1 by A6, NAT_1:13;
hence k < n + 1 by NAT_1:13; :: thesis: ( k < n & k <= n )
thus ( k < n & k <= n ) by A6, NAT_1:13; :: thesis: verum

end;

then ( f . (k + 1) = (f . k) \ (y \ x) & g . (k + 1) = (g . k) \ (y \ x) ) by A1, A2;
hence f . (k + 1) = g . (k + 1) by A5, A7; :: thesis: verum

end;

hence for k being Element of NAT st S₁[k] holds
S₁[k + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
then f . n = g . n ;
hence Polynom m,(n + 1),x,y = (Polynom m,n,x,y) \ (y \ x) by A1, A2, XREAL_1:31; :: thesis: verum