defpred S1[ set ] means for t being Element of F1() st len t = $1 holds
P1[t];
for x being set st card x = 0 holds
x = {} ;
then A3: S1[ 0 ] by A1;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: for t being Element of F1() st len t = k holds
P1[t] ; :: thesis: S1[k + 1]
let t be Element of F1(); :: thesis: ( len t = k + 1 implies P1[t] )
assume len t = k + 1 ; :: thesis: P1[t]
then consider v being FinSequence, x being set such that
A6: t = v ^ <*x*> and
A7: len v = k by Th3;
reconsider v = v as FinSequence of NAT by A6, FINSEQ_1:36;
reconsider v = v as Element of F1() 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: P1[v] by A5, A7;
x = x ;
hence P1[t] by A2, A6, A8; :: thesis: verum
end;
A9: for k being Nat holds S1[k] from NAT_1:sch 2(A3, A4);
 let t be Element of F1(); :: thesis: P1[t]
len t = len t ;
hence P1[t] by A9; :: thesis: verum