{} in {{}} * by FINSEQ_1:49;
then reconsider f = {{}} --> {} as Function of {{}},({{}} *) by FUNCOP_1:46;
reconsider g = {{}} --> {} as Function of {{}},{{}} ;
take c = ManySortedSign(# {{}},{{}},f,g #); :: thesis: ( not c is void & c is Circuit-like & c is strict )
c is Circuit-like

proof

let S be non empty non void ManySortedSign ; :: according to MSAFREE2:def 6 :: thesis: ( S = c implies for o1, o2 being OperSymbol of S st the_result_sort_of o1 = the_result_sort_of o2 holds
o1 = o2 )
assume A1: S = c ; :: thesis: for o1, o2 being OperSymbol of S st the_result_sort_of o1 = the_result_sort_of o2 holds
o1 = o2
let v1, v2 be OperSymbol of S; :: thesis: ( the_result_sort_of v1 = the_result_sort_of v2 implies v1 = v2 )
assume the_result_sort_of v1 = the_result_sort_of v2 ; :: thesis: v1 = v2
thus v1 = {} by A1, TARSKI:def 1
.= v2 by A1, TARSKI:def 1 ; :: thesis: verum

end;

hence ( not c is void & c is Circuit-like & c is strict ) ; :: thesis: verum