set G = DTConOSA X;
set D = bool [:(TS (DTConOSA X)), the carrier of S:];
deffunc H1( Symbol of (DTConOSA X)) -> Subset of [:(TS (DTConOSA X)), the carrier of S:] = @ $1;
deffunc H2( Symbol of (DTConOSA X), set , FinSequence of bool [:(TS (DTConOSA X)), the carrier of S:]) -> Subset of [:(TS (DTConOSA X)), the carrier of S:] = @ ($1,$3);
let f1, f2 be Function of (TS (DTConOSA X)),(bool [:(TS (DTConOSA X)), the carrier of S:]); ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
f1 . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
f1 . (nt -tree ts) = @ (nt,(f1 * ts)) ) & ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
f2 . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
f2 . (nt -tree ts) = @ (nt,(f2 * ts)) ) implies f1 = f2 )
assume that
A1:
( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
f1 . (root-tree t) = H1(t) ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
f1 . (nt -tree ts) = H2(nt, roots ts,f1 * ts) ) )
and
A2:
( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
f2 . (root-tree t) = H1(t) ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
f2 . (nt -tree ts) = H2(nt, roots ts,f2 * ts) ) )
; f1 = f2
thus
f1 = f2
from DTCONSTR:sch 9(A1, A2); verum