let f, x be set ; :: thesis: for p being FinSequence holds

( 1GateCircStr (p,f,x) is gate`1=arity & 1GateCircStr (p,f,x) is Circuit-like )

let p be FinSequence; :: thesis: ( 1GateCircStr (p,f,x) is gate`1=arity & 1GateCircStr (p,f,x) is Circuit-like )

set S = 1GateCircStr (p,f,x);

thus 1GateCircStr (p,f,x) is gate`1=arity :: thesis: 1GateCircStr (p,f,x) is Circuit-like

( 1GateCircStr (p,f,x) is gate`1=arity & 1GateCircStr (p,f,x) is Circuit-like )

let p be FinSequence; :: thesis: ( 1GateCircStr (p,f,x) is gate`1=arity & 1GateCircStr (p,f,x) is Circuit-like )

set S = 1GateCircStr (p,f,x);

thus 1GateCircStr (p,f,x) is gate`1=arity :: thesis: 1GateCircStr (p,f,x) is Circuit-like

proof

thus
1GateCircStr (p,f,x) is Circuit-like
:: thesis: verum
let g be set ; :: according to CIRCCOMB:def 8 :: thesis: ( not g in the carrier' of (1GateCircStr (p,f,x)) or g = [( the Arity of (1GateCircStr (p,f,x)) . g),(g `2)] )

assume g in the carrier' of (1GateCircStr (p,f,x)) ; :: thesis: g = [( the Arity of (1GateCircStr (p,f,x)) . g),(g `2)]

then g in {[p,f]} by CIRCCOMB:def 5;

then A1: g = [p,f] by TARSKI:def 1;

thus g = [( the Arity of (1GateCircStr (p,f,x)) . g),(g `2)] by A1, CIRCCOMB:def 5; :: thesis: verum

end;assume g in the carrier' of (1GateCircStr (p,f,x)) ; :: thesis: g = [( the Arity of (1GateCircStr (p,f,x)) . g),(g `2)]

then g in {[p,f]} by CIRCCOMB:def 5;

then A1: g = [p,f] by TARSKI:def 1;

thus g = [( the Arity of (1GateCircStr (p,f,x)) . g),(g `2)] by A1, CIRCCOMB:def 5; :: thesis: verum

proof

let S9 be non empty non void ManySortedSign ; :: according to MSAFREE2:def 6 :: thesis: ( not S9 = 1GateCircStr (p,f,x) or for b_{1}, b_{2} being Element of the carrier' of S9 holds

( not the_result_sort_of b_{1} = the_result_sort_of b_{2} or b_{1} = b_{2} ) )

assume A2: S9 = 1GateCircStr (p,f,x) ; :: thesis: for b_{1}, b_{2} being Element of the carrier' of S9 holds

( not the_result_sort_of b_{1} = the_result_sort_of b_{2} or b_{1} = b_{2} )

let o1, o2 be OperSymbol of S9; :: thesis: ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 )

o1 = [p,f] by A2, CIRCCOMB:37;

hence ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 ) by A2, CIRCCOMB:37; :: thesis: verum

end;( not the_result_sort_of b

assume A2: S9 = 1GateCircStr (p,f,x) ; :: thesis: for b

( not the_result_sort_of b

let o1, o2 be OperSymbol of S9; :: thesis: ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 )

o1 = [p,f] by A2, CIRCCOMB:37;

hence ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 ) by A2, CIRCCOMB:37; :: thesis: verum