let X be set ; :: thesis: for f, g being Relation of X,X st rng f = X & rng g = X holds
rng (g * f) = X
let f, g be Relation of X,X; :: thesis: ( rng f = X & rng g = X implies rng (g * f) = X )
assume that
A1: rng f = X and
A2: rng g = X ; :: thesis: rng (g * f) = X
thus rng (g * f) = f .: X by A2, RELAT_1:127
.= X by A1, RELSET_1:22 ; :: thesis: verum