A1: support b c= dom b by PRE_POLY:37;
for x being set st x in support b holds
x in X

proof

let x be set ; :: thesis: ( x in support b implies x in X )
assume x in support b ; :: thesis: x in X
then x in dom b by A1;
hence x in X by PARTFUN1:def 2; :: thesis: verum

end;

hence support b is finite Subset of X by TARSKI:def 3; :: thesis: verum