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;
[p,f] `2 = f by MCART_1:7;
hence 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:44;
hence ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 ) by A2, CIRCCOMB:44; :: thesis: verum

end;