let Al be QC-alphabet ; :: thesis: for k, n being Element of NAT st n <= k holds

n -th_FCEx Al c= k -th_FCEx Al

let k be Element of NAT ; :: thesis: for n being Element of NAT st n <= k holds

n -th_FCEx Al c= k -th_FCEx Al

defpred S_{1}[ Nat] means ( $1 <= k implies ex j being Element of NAT st

( j = k - $1 & j -th_FCEx Al c= k -th_FCEx Al ) );

A1: S_{1}[ 0 ]
;

A2: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A1, A2);

let n be Element of NAT ; :: thesis: ( n <= k implies n -th_FCEx Al c= k -th_FCEx Al )

assume A7: n <= k ; :: thesis: n -th_FCEx Al c= k -th_FCEx Al

set n2 = k - n;

reconsider n2 = k - n as Element of NAT by A7, NAT_1:21;

k = n + n2 ;

then consider n3 being Element of NAT such that

A8: ( n3 = k - n2 & n3 -th_FCEx Al c= k -th_FCEx Al ) by A6, NAT_1:11;

thus n -th_FCEx Al c= k -th_FCEx Al by A8; :: thesis: verum

n -th_FCEx Al c= k -th_FCEx Al

let k be Element of NAT ; :: thesis: for n being Element of NAT st n <= k holds

n -th_FCEx Al c= k -th_FCEx Al

defpred S

( j = k - $1 & j -th_FCEx Al c= k -th_FCEx Al ) );

A1: S

A2: for n being Nat st S

S

proof

A6:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A3: S_{1}[n]
; :: thesis: S_{1}[n + 1]

end;assume A3: S

per cases
( n + 1 <= k or not n + 1 <= k )
;

end;

suppose A4:
n + 1 <= k
; :: thesis: S_{1}[n + 1]

then consider j being Element of NAT such that

A5: ( j = k - n & j -th_FCEx Al c= k -th_FCEx Al ) by A3, NAT_1:13;

set j2 = k - (n + 1);

reconsider j2 = k - (n + 1) as Element of NAT by A4, NAT_1:21;

FCEx (j2 -th_FCEx Al) = j -th_FCEx Al by A5, Th5;

then j2 -th_FCEx Al c= j -th_FCEx Al by QC_TRANS:def 1;

hence S_{1}[n + 1]
by A5, XBOOLE_1:1; :: thesis: verum

end;A5: ( j = k - n & j -th_FCEx Al c= k -th_FCEx Al ) by A3, NAT_1:13;

set j2 = k - (n + 1);

reconsider j2 = k - (n + 1) as Element of NAT by A4, NAT_1:21;

FCEx (j2 -th_FCEx Al) = j -th_FCEx Al by A5, Th5;

then j2 -th_FCEx Al c= j -th_FCEx Al by QC_TRANS:def 1;

hence S

let n be Element of NAT ; :: thesis: ( n <= k implies n -th_FCEx Al c= k -th_FCEx Al )

assume A7: n <= k ; :: thesis: n -th_FCEx Al c= k -th_FCEx Al

set n2 = k - n;

reconsider n2 = k - n as Element of NAT by A7, NAT_1:21;

k = n + n2 ;

then consider n3 being Element of NAT such that

A8: ( n3 = k - n2 & n3 -th_FCEx Al c= k -th_FCEx Al ) by A6, NAT_1:11;

thus n -th_FCEx Al c= k -th_FCEx Al by A8; :: thesis: verum