set G = DTConOSA X;
set D = TS (DTConOSA X);
deffunc H₁( Symbol of (DTConOSA X)) -> Element of TS (DTConOSA X) = pi $1;
deffunc H₂( Symbol of (DTConOSA X), set , FinSequence of TS (DTConOSA X)) -> Element of TS (DTConOSA X) = In (pi (@ X,$1),$3),(TS (DTConOSA X));
consider f being Function of (TS (DTConOSA X)),(TS (DTConOSA X)) such that
A1: ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
f . (root-tree t) = H₁(t) ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
f . (nt -tree ts) = H₂(nt, roots ts,f * ts) ) ) from DTCONSTR:sch 8();
take f ; :: thesis: ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
f . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
f . (nt -tree ts) = pi (@ X,nt),(f * ts) ) )
thus for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
f . (root-tree t) = H₁(t) by A1; :: thesis: for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
f . (nt -tree ts) = pi (@ X,nt),(f * ts)
let nt be Symbol of (DTConOSA X); :: thesis: for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
f . (nt -tree ts) = pi (@ X,nt),(f * ts)
let ts be FinSequence of TS (DTConOSA X); :: thesis: ( nt ==> roots ts implies f . (nt -tree ts) = pi (@ X,nt),(f * ts) )
assume A2: nt ==> roots ts ; :: thesis: f . (nt -tree ts) = pi (@ X,nt),(f * ts)
reconsider fts = f * ts as FinSequence of TS (DTConOSA X) ;
f . (nt -tree ts) = In (pi (@ X,nt),fts),(TS (DTConOSA X)) by A1, A2;
hence f . (nt -tree ts) = pi (@ X,nt),(f * ts) by FUNCT_7:def 1; :: thesis: verum