defpred S₁[ set ] means for t being Element of F₁() st len t = $1 holds
P₁[t];
for x being set st card x = 0 holds
x = {} ;
then A3: S₁[ 0 ] by A1;
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: for t being Element of F₁() st len t = k holds
P₁[t] ; :: thesis: S₁[k + 1]
let t be Element of F₁(); :: thesis: ( len t = k + 1 implies P₁[t] )
assume len t = k + 1 ; :: thesis: P₁[t]
then consider v being FinSequence, x being set such that
A6: t = v ^ <*x*> and
A7: len v = k by Th4;
reconsider v = v as FinSequence of NAT by A6, FINSEQ_1:36;
reconsider v = v as Element of F₁() by A6, TREES_1:21;
rng <*x*> c= rng t by A6, FINSEQ_1:30;
then ( rng <*x*> = {x} & rng <*x*> c= NAT ) by FINSEQ_1:39, XBOOLE_1:1;
then reconsider x = x as Element of NAT by ZFMISC_1:31;
A8: P₁[v] by A5, A7;
x = x ;
hence P₁[t] by A2, A6, A8; :: thesis: verum

end;

A9: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4);
let t be Element of F₁(); :: thesis: P₁[t]
len t = len t ;
hence P₁[t] by A9; :: thesis: verum