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 4;
rng (FuncComp {(id o)},{(id o)}) c= {(id o)}

proof

let i be set ; :: 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 set such that
A2: j in [:{(id o)},{(id o)}:] and
A3: i = (FuncComp {(id o)},{(id o)}) . j by A1, FUNCT_1:def 5;
consider f, g being Function such that
A4: j = [g,f] and
A5: (FuncComp {(id o)},{(id o)}) . j = g * f by A1, A2, Def11;
f in {(id o)} by A2, A4, ZFMISC_1:106;
then A6: f = id o by TARSKI:def 1;
g in {(id o)} by A2, A4, ZFMISC_1:106;
then ( o /\ o = o & g = id o ) by TARSKI:def 1;
then i = id o by A3, A5, A6, FUNCT_1:43;
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:11;
hence FuncComp {(id o)},{(id o)} = (id o),(id o) :-> (id o) by FUNCOP_1:def 10; :: thesis: verum