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= {}

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

hence
(ff_0 f) . {} = {}
by Defff; :: thesis: verum
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;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