A3: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
proof
let nt be Symbol of F1(); :: thesis: for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]

let ts be FinSequence of TS F1(); :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
P1[t] ) implies P1[nt -tree ts] )

assume that
A4: nt ==> roots ts and
A5: for t being DecoratedTree of the carrier of F1() st t in rng ts holds
P1[t] ; :: thesis: P1[nt -tree ts]
A6: nt is NonTerminal of F1() by ;
consider tl, tr being Element of TS F1() such that
A7: roots ts = <*(),()*> and
tl = ts . 1 and
tr = ts . 2 and
A8: nt -tree ts = nt -tree (tl,tr) and
A9: ( tl in rng ts & tr in rng ts ) by ;
( P1[tl] & P1[tr] ) by A5, A9;
hence P1[nt -tree ts] by A2, A4, A6, A7, A8; :: thesis: verum
end;
A10: for s being Symbol of F1() st s in Terminals F1() holds
P1[ root-tree s] by A1;
for t being DecoratedTree of the carrier of F1() st t in TS F1() holds
P1[t] from hence for t being Element of TS F1() holds P1[t] ; :: thesis: verum