let S, T be non empty RelStr ; :: thesis: for g being Function of S,T
for d being Function of T,S st g = (g * d) * g holds
g * d is idempotent
let g be Function of S,T; :: thesis: for d being Function of T,S st g = (g * d) * g holds
g * d is idempotent
let d be Function of T,S; :: thesis: ( g = (g * d) * g implies g * d is idempotent )
assume g = (g * d) * g ; :: thesis: g * d is idempotent
hence (g * d) * (g * d) = g * d by RELAT_1:36; :: according to QUANTAL1:def 9 :: thesis: verum