per cases ( not i in dom s or i in dom s ) ;

suppose not i in dom s ; :: thesis: s . i is Element of BOOLEAN

then s . i = {} by FUNCT_1:def 2;
hence s . i is Element of BOOLEAN by TARSKI:def 2; :: thesis: verum

end;

suppose i in dom s ; :: thesis: s . i is Element of BOOLEAN

then s . i in rng s by FUNCT_1:3;
hence s . i is Element of BOOLEAN ; :: thesis: verum

end;

end;