let A, B, C be set ; :: thesis: rng (FuncComp ((Funcs (A,B)),(Funcs (B,C)))) c= Funcs (A,C)
let i be object ; :: 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 object 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 3;
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, Def9;
( g in Funcs (B,C) & f in Funcs (A,B) ) by A1, A3, ZFMISC_1:87;
hence i in Funcs (A,C) by A2, A4, FUNCT_2:128; :: thesis: verum