let R be non empty RelStr ; :: thesis: for f being map of R holds
( f . {} = {} iff (Flip f) . the carrier of R = the carrier of R )
let f be map of R; :: thesis: ( f . {} = {} iff (Flip f) . the carrier of R = the carrier of R )
thus ( f . {} = {} implies (Flip f) . the carrier of R = the carrier of R ) by ROUGHS_2:18; :: thesis: ( (Flip f) . the carrier of R = the carrier of R implies f . {} = {} )
set g = Flip f;
A1: Flip (Flip f) = f by ROUGHS_2:23;
thus ( (Flip f) . the carrier of R = the carrier of R implies f . {} = {} ) by A1, ROUGHS_2:19; :: thesis: verum