{} 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 #); ( 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 )
; verum