let f be set ; :: thesis: for p being FinSequence holds
( 1GateCircStr p,f is unsplit & 1GateCircStr p,f is gate`1=arity )
let p be FinSequence; :: thesis: ( 1GateCircStr p,f is unsplit & 1GateCircStr p,f is gate`1=arity )
set S = 1GateCircStr p,f;
A1: ( the carrier' of (1GateCircStr p,f) = {[p,f]} & the ResultSort of (1GateCircStr p,f) . [p,f] = [p,f] ) by Def6;
then A2: dom the ResultSort of (1GateCircStr p,f) = {[p,f]} by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in {[p,f]} implies the ResultSort of (1GateCircStr p,f) . x = x )
assume x in {[p,f]} ; :: thesis: the ResultSort of (1GateCircStr p,f) . x = x
then x = [p,f] by TARSKI:def 1;
hence the ResultSort of (1GateCircStr p,f) . x = x by Def6; :: thesis: verum

end;

hence the ResultSort of (1GateCircStr p,f) = id the carrier' of (1GateCircStr p,f) by A1, A2, FUNCT_1:34; :: according to CIRCCOMB:def 7 :: thesis: 1GateCircStr p,f is gate`1=arity
let g be set ; :: according to CIRCCOMB:def 8 :: thesis: ( g in the carrier' of (1GateCircStr p,f) implies g = [(the Arity of (1GateCircStr p,f) . g),(g `2 )] )
assume g in the carrier' of (1GateCircStr p,f) ; :: thesis: g = [(the Arity of (1GateCircStr p,f) . g),(g `2 )]
then A3: g = [p,f] by A1, TARSKI:def 1;
then the Arity of (1GateCircStr p,f) . g = p by Def6;
hence g = [(the Arity of (1GateCircStr p,f) . g),(g `2 )] by A3, MCART_1:7; :: thesis: verum