let T be non empty RelStr ; :: thesis: for S being non empty SubRelStr of T
for f being Function of T,S st f * (incl (S,T)) = id S holds
f is idempotent Function of T,T
let S be non empty SubRelStr of T; :: thesis: for f being Function of T,S st f * (incl (S,T)) = id S holds
f is idempotent Function of T,T
let f be Function of T,S; :: thesis: ( f * (incl (S,T)) = id S implies f is idempotent Function of T,T )
assume A1: f * (incl (S,T)) = id S ; :: thesis: f is idempotent Function of T,T
A2: the carrier of S c= the carrier of T by YELLOW_0:def 13;
then incl (S,T) = id the carrier of S by YELLOW_9:def 1;
then (incl (S,T)) * f = f by FUNCT_2:17;
then A3: f * f = (id the carrier of S) * f by A1, RELAT_1:36
.= f by FUNCT_2:17 ;
A4: dom f = the carrier of T by FUNCT_2:def 1;
f is onto by A1, FUNCT_2:23;
then rng f = the carrier of S by FUNCT_2:def 3;
hence f is idempotent Function of T,T by A2, A3, A4, FUNCT_2:2, QUANTAL1:def 9; :: thesis: verum