let X be BCI-algebra; for x, y, z being Element of X
for n being Nat holds ((x,z) to_power n) \ ((y,z) to_power n) <= x \ y
let x, y, z be Element of X; for n being Nat holds ((x,z) to_power n) \ ((y,z) to_power n) <= x \ y
let n be Nat; ((x,z) to_power n) \ ((y,z) to_power n) <= x \ y
defpred S1[ set ] means for m being Nat st m = $1 & m <= n holds
((x,z) to_power m) \ ((y,z) to_power m) <= x \ y;
A1:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A2:
for
m being
Nat st
m = k &
m <= n holds
((x,z) to_power m) \ ((y,z) to_power m) <= x \ y
;
S1[k + 1]
let m be
Nat;
( m = k + 1 & m <= n implies ((x,z) to_power m) \ ((y,z) to_power m) <= x \ y )
assume that A3:
m = k + 1
and A4:
m <= n
;
((x,z) to_power m) \ ((y,z) to_power m) <= x \ y
k <= n
by A3, A4, NAT_1:13;
then
((x,z) to_power k) \ ((y,z) to_power k) <= x \ y
by A2;
then
(((x,z) to_power k) \ ((y,z) to_power k)) \ (x \ y) = 0. X
;
then
(((x,z) to_power k) \ (x \ y)) \ ((y,z) to_power k) = 0. X
by BCIALG_1:7;
then
((((x,z) to_power k) \ (x \ y)) \ z) \ (((y,z) to_power k) \ z) = 0. X
by BCIALG_1:4;
then
((((x,z) to_power k) \ z) \ (x \ y)) \ (((y,z) to_power k) \ z) = 0. X
by BCIALG_1:7;
then
(((x,z) to_power (k + 1)) \ (x \ y)) \ (((y,z) to_power k) \ z) = 0. X
by Th4;
then
(((x,z) to_power (k + 1)) \ (x \ y)) \ ((y,z) to_power (k + 1)) = 0. X
by Th4;
then
(((x,z) to_power (k + 1)) \ ((y,z) to_power (k + 1))) \ (x \ y) = 0. X
by BCIALG_1:7;
hence
((x,z) to_power m) \ ((y,z) to_power m) <= x \ y
by A3;
verum
end;
(x \ y) \ (x \ y) = 0. X
by BCIALG_1:def 5;
then
x \ y <= x \ y
;
then
((x,z) to_power 0) \ y <= x \ y
by Th1;
then A5:
S1[ 0 ]
by Th1;
for n being Nat holds S1[n]
from NAT_1:sch 2(A5, A1);
hence
((x,z) to_power n) \ ((y,z) to_power n) <= x \ y
; verum