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

( 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