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

proof

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;

thus 1GateCircStr (p,f,x) is Circuit-like :: 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₁, b₂ being Element of the carrier' of S9 holds
( not the_result_sort_of b₁ = the_result_sort_of b₂ or b₁ = b₂ ) )
assume A2: S9 = 1GateCircStr (p,f,x) ; :: thesis: for b₁, b₂ being Element of the carrier' of S9 holds
( not the_result_sort_of b₁ = the_result_sort_of b₂ or b₁ = 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

end;