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 object such that
A3: g in Funcs (B,C) by A2, XBOOLE_0:def 1;
ex f being object st f in Funcs (A,B) by A1, XBOOLE_0:def 1;
hence Funcs (A,C) <> {} by A3, Th127; :: thesis: verum