{} in {{} ,{{} }} by TARSKI:def 2;
then reconsider g = {{} } --> {} as Function of {{} },{{} ,{{} }} by FUNCOP_1:58;
{} in {{} ,{{} }} * by FINSEQ_1:66;
then reconsider f = {{} } --> {} as Function of {{} },({{} ,{{} }} * ) by FUNCOP_1:58;
take c = ManySortedSign(# {{} ,{{} }},{{} },f,g #); :: thesis: ( not c is void & c is with_input_V )
rng the ResultSort of c = {{} } by FUNCOP_1:14;
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 ) by Def4; :: thesis: verum