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)) )
reconsider fts = f * ts as FinSequence of TS (DTConOSA X) ;
assume nt ==> roots ts ; :: thesis: f . (nt -tree ts) = pi ((@ (X,nt)),(f * ts))
then f . (nt -tree ts) = In ((pi ((@ (X,nt)),fts)),(TS (DTConOSA X))) by A1;
hence f . (nt -tree ts) = pi ((@ (X,nt)),(f * ts)) ; :: thesis: verum