let f be Function; :: thesis: support f c= dom f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support f or x in dom f )
assume x in support f ; :: thesis: x in dom f
then f . x <> 0 by Def7;
hence x in dom f by FUNCT_1:def 2; :: thesis: verum