let C be initialized ConstructorSignature; for t being set holds
( t in Terminals (DTConMSA (MSVars C)) iff ex x being variable st t = [x,(a_Term C)] )
let t be set ; ( t in Terminals (DTConMSA (MSVars C)) iff ex x being variable st t = [x,(a_Term C)] )
set X = MSVars C;
A1:
Terminals (DTConMSA (MSVars C)) = Union (coprod (MSVars C))
by Th120;
A2:
dom (MSVars C) = the carrier of C
by PARTFUN1:def 2;
A3:
the carrier of C = {a_Type,an_Adj,a_Term}
by Def9;
A4:
(MSVars C) . a_Type = {}
by Def25;
A5:
(MSVars C) . an_Adj = {}
by Def25;
A6:
(MSVars C) . a_Term = Vars
by Def25;
hereby ( ex x being variable st t = [x,(a_Term C)] implies t in Terminals (DTConMSA (MSVars C)) )
assume A7:
t in Terminals (DTConMSA (MSVars C))
;
ex x being variable st t = [x,(a_Term C)]then A8:
t `2 in dom (MSVars C)
by A1, CARD_3:22;
A9:
t `1 in (MSVars C) . (t `2)
by A1, A7, CARD_3:22;
A10:
(
t `2 = a_Type or
t `2 = an_Adj or
t `2 = a_Term )
by A3, A8, ENUMSET1:def 1;
reconsider x =
t `1 as
variable by A3, A4, A5, A6, A8, A9, ENUMSET1:def 1;
take x =
x;
t = [x,(a_Term C)]thus
t = [x,(a_Term C)]
by A1, A4, A5, A7, A10, CARD_3:22;
verum
end;
given x being variable such that A11:
t = [x,(a_Term C)]
; t in Terminals (DTConMSA (MSVars C))
A12:
t `1 = x
by A11;
t `2 = a_Term
by A11;
hence
t in Terminals (DTConMSA (MSVars C))
by A1, A2, A6, A11, A12, CARD_3:22; verum