let X be BCI-algebra; :: thesis: for n, j, m being Element of NAT st X is p-Semisimple BCI-algebra holds
X is BCI-algebra of n + j,n,m,(m + j) + 1
let n, j, m be Element of 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₁[ Element of NAT ] means ( $1 <= n implies Polynom $1,$1,x,y = y );

now

let k be Element of 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 Element of 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 Element of NAT holds S₁[n] from NAT_1:sch 1(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₁[ Element of NAT ] means ( $1 <= m implies Polynom $1,($1 + 1),x,y = x );

now

let k be Element of 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 Element of 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 Element of NAT holds S₁[m] from NAT_1:sch 1(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₁[ Element of NAT ] means ( $1 <= j implies Polynom (n + $1),n,x,y = Polynom m,((m + $1) + 1),y,x );

now

let k be Element of 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 Element of 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 Element of NAT holds S₁[j] from NAT_1:sch 1(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