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) = pi ((@ (X,$1)),$3);
let M1, M2 be Function of (TS (DTConOSA X)),(TS (DTConOSA X)); :: thesis: ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
M1 . (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
M1 . (nt -tree ts) = pi ((@ (X,nt)),(M1 * ts)) ) & ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
M2 . (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
M2 . (nt -tree ts) = pi ((@ (X,nt)),(M2 * ts)) ) implies M1 = M2 )
assume that
A2: ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
M1 . (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
M1 . (nt -tree ts) = H₂(nt, roots ts,M1 * ts) ) ) and
A3: ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
M2 . (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
M2 . (nt -tree ts) = H₂(nt, roots ts,M2 * ts) ) ) ; :: thesis: M1 = M2
thus M1 = M2 from DTCONSTR:sch 9(A2, A3); :: thesis: verum