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
then A2: rng f = the carrier of S by FUNCT_2:29;
A3: 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:23;
then A4: f * f = (id the carrier of S) * f by A1, RELAT_1:55
.= f by FUNCT_2:23 ;
dom f = the carrier of T by FUNCT_2:def 1;
hence f is idempotent Function of T,T by A2, A3, A4, FUNCT_2:4, QUANTAL1:def 9; :: thesis: verum