let A, B, C be set ; :: thesis: rng (FuncComp (Funcs A,B),(Funcs B,C)) c= Funcs A,C
let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in rng (FuncComp (Funcs A,B),(Funcs B,C)) or i in Funcs A,C )
set F = FuncComp (Funcs A,B),(Funcs B,C);
assume i in rng (FuncComp (Funcs A,B),(Funcs B,C)) ; :: thesis: i in Funcs A,C
then consider j being set such that
A1: j in dom (FuncComp (Funcs A,B),(Funcs B,C)) and
A2: i = (FuncComp (Funcs A,B),(Funcs B,C)) . j by FUNCT_1:def 5;
consider f, g being Function such that
A3: j = [g,f] and
A4: (FuncComp (Funcs A,B),(Funcs B,C)) . j = g * f by A1, Def11;
dom (FuncComp (Funcs A,B),(Funcs B,C)) = [:(Funcs B,C),(Funcs A,B):] by PARTFUN1:def 4;
then ( g in Funcs B,C & f in Funcs A,B ) by A1, A3, ZFMISC_1:106;
hence i in Funcs A,C by A2, A4, Th4; :: thesis: verum