let o be set ; :: thesis: FuncComp ({(id o)},{(id o)}) = ((id o),(id o)) :-> (id o)
A1: dom (FuncComp ({(id o)},{(id o)})) = [:{(id o)},{(id o)}:] by PARTFUN1:def 2;
rng (FuncComp ({(id o)},{(id o)})) c= {(id o)}

proof

let i be object ; :: according to TARSKI:def 3 :: thesis: ( not i in rng (FuncComp ({(id o)},{(id o)})) or i in {(id o)} )
assume i in rng (FuncComp ({(id o)},{(id o)})) ; :: thesis: i in {(id o)}
then consider j being object such that
A2: j in [:{(id o)},{(id o)}:] and
A3: i = (FuncComp ({(id o)},{(id o)})) . j by A1, FUNCT_1:def 3;
consider f, g being Function such that
A4: j = [g,f] and
A5: (FuncComp ({(id o)},{(id o)})) . j = g * f by A1, A2, Def9;
f in {(id o)} by A2, A4, ZFMISC_1:87;
then A6: f = id o by TARSKI:def 1;
g in {(id o)} by A2, A4, ZFMISC_1:87;
then ( o /\ o = o & g = id o ) by TARSKI:def 1;
then i = id o by A3, A5, A6, FUNCT_1:22;
hence i in {(id o)} by TARSKI:def 1; :: thesis: verum

end;

then FuncComp ({(id o)},{(id o)}) is Function of [:{(id o)},{(id o)}:],{(id o)} by A1, RELSET_1:4;
hence FuncComp ({(id o)},{(id o)}) = ((id o),(id o)) :-> (id o) by FUNCOP_1:def 10; :: thesis: verum