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