let X be BCI-algebra; :: thesis: for j, m, n being Nat st X is p-Semisimple BCI-algebra holds
X is BCI-algebra of n + j,n,m,(m + j) + 1
let j, m, n be Nat; :: thesis: ( X is p-Semisimple BCI-algebra implies X is BCI-algebra of n + j,n,m,(m + j) + 1 )
assume A1: X is p-Semisimple BCI-algebra ; :: thesis: X is BCI-algebra of n + j,n,m,(m + j) + 1
A2: for x, y being Element of X holds Polynom (n,n,x,y) = y

proof

let x, y be Element of X; :: thesis: Polynom (n,n,x,y) = y
defpred S₁[ Nat] means ( $1 <= n implies Polynom ($1,$1,x,y) = y );

now :: thesis: for k being Nat st ( k <= n implies Polynom (k,k,x,y) = y ) & k + 1 <= n holds
Polynom ((k + 1),(k + 1),x,y) = y

let k be Nat; :: thesis: ( ( k <= n implies Polynom (k,k,x,y) = y ) & k + 1 <= n implies Polynom ((k + 1),(k + 1),x,y) = y )
assume A3: ( k <= n implies Polynom (k,k,x,y) = y ) ; :: thesis: ( k + 1 <= n implies Polynom ((k + 1),(k + 1),x,y) = y )
set m = k + 1;
A4: Polynom ((k + 1),(k + 1),x,y) = (Polynom (k,(k + 1),x,y)) \ (x \ y) by Th9
.= ((Polynom (k,k,x,y)) \ (y \ x)) \ (x \ y) by Th10 ;
assume k + 1 <= n ; :: thesis: Polynom ((k + 1),(k + 1),x,y) = y
then Polynom ((k + 1),(k + 1),x,y) = x \ (x \ y) by A1, A3, A4, BCIALG_1:def 26, NAT_1:13;
hence Polynom ((k + 1),(k + 1),x,y) = y by A1, BCIALG_1:def 26; :: thesis: verum

end;

then A5: for k being Nat st S₁[k] holds
S₁[k + 1] ;
Polynom (0,0,x,y) = x \ (x \ y) by Th7
.= y by A1, BCIALG_1:def 26 ;
then A6: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A5);
hence Polynom (n,n,x,y) = y ; :: thesis: verum

end;

A7: for x, y being Element of X holds Polynom (m,(m + 1),x,y) = x

proof

let x, y be Element of X; :: thesis: Polynom (m,(m + 1),x,y) = x
defpred S₁[ Nat] means ( $1 <= m implies Polynom ($1,($1 + 1),x,y) = x );

now :: thesis: for k being Nat st ( k <= m implies Polynom (k,(k + 1),x,y) = x ) & k + 1 <= m holds
Polynom ((k + 1),((k + 1) + 1),x,y) = x

let k be Nat; :: thesis: ( ( k <= m implies Polynom (k,(k + 1),x,y) = x ) & k + 1 <= m implies Polynom ((k + 1),((k + 1) + 1),x,y) = x )
assume A8: ( k <= m implies Polynom (k,(k + 1),x,y) = x ) ; :: thesis: ( k + 1 <= m implies Polynom ((k + 1),((k + 1) + 1),x,y) = x )
set l = k + 1;
A9: Polynom ((k + 1),((k + 1) + 1),x,y) = (Polynom (k,((k + 1) + 1),x,y)) \ (x \ y) by Th9
.= ((Polynom (k,(k + 1),x,y)) \ (y \ x)) \ (x \ y) by Th10 ;
assume k + 1 <= m ; :: thesis: Polynom ((k + 1),((k + 1) + 1),x,y) = x
then Polynom ((k + 1),((k + 1) + 1),x,y) = (x \ (x \ y)) \ (y \ x) by A8, A9, BCIALG_1:7, NAT_1:13
.= y \ (y \ x) by A1, BCIALG_1:def 26 ;
hence Polynom ((k + 1),((k + 1) + 1),x,y) = x by A1, BCIALG_1:def 26; :: thesis: verum

end;

then A10: for k being Nat st S₁[k] holds
S₁[k + 1] ;
Polynom (0,1,x,y) = (Polynom (0,0,x,y)) \ (y \ x) by Th10
.= (x \ (x \ y)) \ (y \ x) by Th7
.= y \ (y \ x) by A1, BCIALG_1:def 26
.= x by A1, BCIALG_1:def 26 ;
then A11: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A11, A10);
hence Polynom (m,(m + 1),x,y) = x ; :: thesis: verum

end;

for x, y being Element of X holds Polynom ((n + j),n,x,y) = Polynom (m,((m + j) + 1),y,x)

proof

let x, y be Element of X; :: thesis: Polynom ((n + j),n,x,y) = Polynom (m,((m + j) + 1),y,x)
defpred S₁[ Nat] means ( $1 <= j implies Polynom ((n + $1),n,x,y) = Polynom (m,((m + $1) + 1),y,x) );

now :: thesis: for k being Nat st ( k <= j implies Polynom ((n + k),n,x,y) = Polynom (m,((m + k) + 1),y,x) ) & k + 1 <= j holds
Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x)

let k be Nat; :: thesis: ( ( k <= j implies Polynom ((n + k),n,x,y) = Polynom (m,((m + k) + 1),y,x) ) & k + 1 <= j implies Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x) )
assume A12: ( k <= j implies Polynom ((n + k),n,x,y) = Polynom (m,((m + k) + 1),y,x) ) ; :: thesis: ( k + 1 <= j implies Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x) )
set l = k + 1;
assume k + 1 <= j ; :: thesis: Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x)
then Polynom ((n + (k + 1)),n,x,y) = (Polynom (m,((m + k) + 1),y,x)) \ (x \ y) by A12, Th9, NAT_1:13
.= Polynom (m,(((m + k) + 1) + 1),y,x) by Th10 ;
hence Polynom ((n + (k + 1)),n,x,y) = Polynom (m,((m + (k + 1)) + 1),y,x) ; :: thesis: verum

end;

then A13: for k being Nat st S₁[k] holds
S₁[k + 1] ;
Polynom ((n + 0),n,x,y) = y by A2
.= Polynom (m,((m + 0) + 1),y,x) by A7 ;
then A14: S₁[ 0 ] ;
for j being Nat holds S₁[j] from NAT_1:sch 2(A14, A13);
hence Polynom ((n + j),n,x,y) = Polynom (m,((m + j) + 1),y,x) ; :: thesis: verum

end;

hence X is BCI-algebra of n + j,n,m,(m + j) + 1 by Def3; :: thesis: verum