let T be non empty RelStr ; 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; 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; ( f * (incl (S,T)) = id S implies f is idempotent Function of T,T )
assume A1:
f * (incl (S,T)) = id S
; 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; verum