let R be non empty RelStr ; :: thesis: for f being Function of the carrier of R,(bool the carrier of R) holds (ff_0 f) . {} = {}
let f be Function of the carrier of R,(bool the carrier of R); :: thesis: (ff_0 f) . {} = {}
{ u where u is Element of R : f . u meets {} R } c= {}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { u where u is Element of R : f . u meets {} R } or y in {} )
assume y in { u where u is Element of R : f . u meets {} R } ; :: thesis: y in {}
then consider u being Element of R such that
A1: ( u = y & f . u meets {} R ) ;
thus y in {} by A1; :: thesis: verum

end;

hence (ff_0 f) . {} = {} by Defff; :: thesis: verum