let A, B, C be set ; :: thesis: ( Funcs A,B <> {} & Funcs B,C <> {} implies Funcs A,C <> {} )
assume that
A1: Funcs A,B <> {} and
A2: Funcs B,C <> {} ; :: thesis: Funcs A,C <> {}
consider f being set such that
A3: f in Funcs A,B by A1, XBOOLE_0:def 1;
consider g being set such that
A4: g in Funcs B,C by A2, XBOOLE_0:def 1;
reconsider f = f as Function of A,B by A3, FUNCT_2:121;
reconsider g = g as Function of B,C by A4, FUNCT_2:121;
g * f in Funcs A,C by A3, A4, Th4;
hence Funcs A,C <> {} ; :: thesis: verum