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 g being set such that
A3: g in Funcs B,C by A2, XBOOLE_0:def 1;
reconsider g = g as Function of B,C by A3, FUNCT_2:121;
consider f being set such that
A4: f in Funcs A,B by A1, XBOOLE_0:def 1;
thus Funcs A,C <> {} by A4, A3, Th4; :: thesis: verum
reconsider f = f as Function of A,B by A4, FUNCT_2:121;