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₁[ 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₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]

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

suppose A4: n + 1 <= k ; :: thesis: S₁[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₁[n + 1] by A5, XBOOLE_1:1; :: thesis: verum

end;

suppose not n + 1 <= k ; :: thesis: S₁[n + 1]

hence S₁[n + 1] ; :: thesis: verum

end;

end;

end;

A6: for n being Nat holds S₁[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