per cases ( not x in dom f or x in dom f ) ;

suppose not x in dom f ; :: thesis: f . x is boolean

then f . x = FALSE by FUNCT_1:def 2;
hence f . x in BOOLEAN ; :: according to MARGREL1:def 12 :: thesis: verum

end;

suppose A1: x in dom f ; :: thesis: f . x is boolean

A2: rng f c= BOOLEAN by Def16;
f . x in rng f by A1, FUNCT_1:def 3;
hence f . x in BOOLEAN by A2; :: according to MARGREL1:def 12 :: thesis: verum

end;

end;