defpred S₁[ set ] means for t being Element of F₁() st len t = $1 holds
P₁[t];
A3: for x being set st card x = 0 holds
x = {} ;
A4: S₁[ 0 ] by A1, A3;
A5: 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 A6: 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 A7: len t = k + 1 ; :: thesis: P₁[t]
consider v being FinSequence, x being set such that
A8: t = v ^ <*x*> and
A9: len v = k by A7, Th4;
reconsider v = v as FinSequence of NAT by A8, FINSEQ_1:50;
reconsider v = v as Element of F₁() by A8, TREES_1:46;
A10: rng <*x*> c= rng t by A8, FINSEQ_1:43;
A11: ( rng <*x*> = {x} & rng <*x*> c= NAT ) by A10, FINSEQ_1:56, XBOOLE_1:1;
reconsider x = x as Element of NAT by A11, ZFMISC_1:37;
A12: P₁[v] by A6, A9;
A13: x = x ;
thus P₁[t] by A2, A8, A12, A13; :: thesis: verum

end;

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