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

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

hence
( not c is void & c is Circuit-like & c is strict )
; :: thesis: verum
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;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