{} in {{},{{}}}
by TARSKI:def 2;

then reconsider g = {{}} --> {} as Function of {{}},{{},{{}}} by FUNCOP_1:46;

{} in {{},{{}}} * by FINSEQ_1:49;

then reconsider f = {{}} --> {} as Function of {{}},({{},{{}}} *) by FUNCOP_1:46;

take c = ManySortedSign(# {{},{{}}},{{}},f,g #); :: thesis: ( not c is void & c is with_input_V )

rng the ResultSort of c = {{}} by FUNCOP_1:8;

then ( {{}} in the carrier of c & not {{}} in rng the ResultSort of c ) by TARSKI:def 2;

then InputVertices c <> {} by XBOOLE_0:def 5;

hence ( not c is void & c is with_input_V ) ; :: thesis: verum

then reconsider g = {{}} --> {} as Function of {{}},{{},{{}}} by FUNCOP_1:46;

{} in {{},{{}}} * by FINSEQ_1:49;

then reconsider f = {{}} --> {} as Function of {{}},({{},{{}}} *) by FUNCOP_1:46;

take c = ManySortedSign(# {{},{{}}},{{}},f,g #); :: thesis: ( not c is void & c is with_input_V )

rng the ResultSort of c = {{}} by FUNCOP_1:8;

then ( {{}} in the carrier of c & not {{}} in rng the ResultSort of c ) by TARSKI:def 2;

then InputVertices c <> {} by XBOOLE_0:def 5;

hence ( not c is void & c is with_input_V ) ; :: thesis: verum