let X be BCI-algebra; :: thesis: for x, y being Element of X
for n, m being Element of NAT holds (x,y to_power n),y to_power m = x,y to_power (n + m)
let x, y be Element of X; :: thesis: for n, m being Element of NAT holds (x,y to_power n),y to_power m = x,y to_power (n + m)
let n, m be Element of NAT ; :: thesis: (x,y to_power n),y to_power m = x,y to_power (n + m)
defpred S1[ set ] means for m1 being Element of NAT st m1 = $1 & m1 <= n holds
(x,y to_power m1),y to_power m = x,y to_power (m1 + m);
A1:
S1[ 0 ]
by Th1;
A2:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
now let k be
Element of
NAT ;
:: thesis: ( ( for m1 being Element of NAT st m1 = k & m1 <= n holds
(x,y to_power m1),y to_power m = x,y to_power (m1 + m) ) implies for m1 being Element of NAT st m1 = k + 1 & m1 <= n holds
(x,y to_power m1),y to_power m = x,y to_power (m1 + m) )assume A3:
for
m1 being
Element of
NAT st
m1 = k &
m1 <= n holds
(x,y to_power m1),
y to_power m = x,
y to_power (m1 + m)
;
:: thesis: for m1 being Element of NAT st m1 = k + 1 & m1 <= n holds
(x,y to_power m1),y to_power m = x,y to_power (m1 + m)let m1 be
Element of
NAT ;
:: thesis: ( m1 = k + 1 & m1 <= n implies (x,y to_power m1),y to_power m = x,y to_power (m1 + m) )assume A4:
(
m1 = k + 1 &
m1 <= n )
;
:: thesis: (x,y to_power m1),y to_power m = x,y to_power (m1 + m)then
k <= n
by NAT_1:13;
then
(x,y to_power k),
y to_power m = x,
y to_power (k + m)
by A3;
then
((x,y to_power k),y to_power m) \ y = x,
y to_power ((k + m) + 1)
by Th4;
then
((x,y to_power k) \ y),
y to_power m = x,
y to_power ((k + m) + 1)
by Th7;
hence
(x,y to_power m1),
y to_power m = x,
y to_power (m1 + m)
by A4, Th4;
:: thesis: verum end;
hence
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
;
:: thesis: verum
end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A1, A2);
hence
(x,y to_power n),y to_power m = x,y to_power (n + m)
; :: thesis: verum