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
A3: ( ( 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
A4: ( ( 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(A3, A4); :: thesis: verum