{} 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