let C be initialized ConstructorSignature; :: thesis: for X being Subset of Vars holds
( dom (C idval X) = X & ( for x being variable st x in X holds
(C idval X) . x = x -term C ) )
let X be Subset of Vars; :: thesis: ( dom (C idval X) = X & ( for x being variable st x in X holds
(C idval X) . x = x -term C ) )
set f = C idval X;
thus dom (C idval X) c= X :: according to XBOOLE_0:def 10 :: thesis: ( X c= dom (C idval X) & ( for x being variable st x in X holds
(C idval X) . x = x -term C ) )

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom (C idval X) or a in X )
assume a in dom (C idval X) ; :: thesis: a in X
then [a,((C idval X) . a)] in C idval X by FUNCT_1:def 2;
then ex x being variable st
( [a,((C idval X) . a)] = [x,(x -term C)] & x in X ) ;
hence a in X by XTUPLE_0:1; :: thesis: verum

end;

hereby :: according to TARSKI:def 3 :: thesis: for x being variable st x in X holds
(C idval X) . x = x -term C

let x be object ; :: thesis: ( x in X implies x in dom (C idval X) )
assume A1: x in X ; :: thesis: x in dom (C idval X)
then reconsider a = x as variable ;
[a,(a -term C)] in C idval X by A1;
hence x in dom (C idval X) by FUNCT_1:1; :: thesis: verum

end;

let x be variable; :: thesis: ( x in X implies (C idval X) . x = x -term C )
assume x in X ; :: thesis: (C idval X) . x = x -term C
then [x,(x -term C)] in C idval X ;
hence (C idval X) . x = x -term C by FUNCT_1:1; :: thesis: verum