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 ( g = [p,f] & [p,f] `2 = f ) by MCART_1:7, TARSKI:def 1;
hence g = [(the Arity of (1GateCircStr p,f,x) . g),(g `2 )] by CIRCCOMB:def 5; :: thesis: verum

end;

thus 1GateCircStr p,f,x is Circuit-like :: thesis: verum

proof

let S' be non empty non void ManySortedSign ; :: according to MSAFREE2:def 6 :: thesis: ( not S' = 1GateCircStr p,f,x or for b₁, b₂ being Element of the carrier' of S' holds
( not the_result_sort_of b₁ = the_result_sort_of b₂ or b₁ = b₂ ) )
assume A1: S' = 1GateCircStr p,f,x ; :: thesis: for b₁, b₂ being Element of the carrier' of S' holds
( not the_result_sort_of b₁ = the_result_sort_of b₂ or b₁ = b₂ )
let o1, o2 be OperSymbol of S'; :: thesis: ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 )
( o1 = [p,f] & o2 = [p,f] ) by A1, CIRCCOMB:44;
hence ( not the_result_sort_of o1 = the_result_sort_of o2 or o1 = o2 ) ; :: thesis: verum

end;