{} in {{} ,{{} }} * by FINSEQ_1:66;
then reconsider f = {{} } --> {} as Function of {{} },({{} ,{{} }} * ) by FUNCOP_1:58;
{} in {{} ,{{} }} by TARSKI:def 2;
then reconsider g = {{} } --> {} as Function of {{} },{{} ,{{} }} by FUNCOP_1:58;
take c = ManySortedSign(# {{} ,{{} }},{{} },f,g #); :: thesis: ( not c is void & c is with_input_V )
c is with_input_V

proof

A1: {{} } in the carrier of c by TARSKI:def 2;
rng the ResultSort of c = {{} } by FUNCOP_1:14;
then not {{} } in rng the ResultSort of c ;
then InputVertices c <> {} by A1, XBOOLE_0:def 5;
hence c is with_input_V by Def4; :: thesis: verum

end;

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