let f be object ; :: 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: now :: thesis: for x being object st x in {[p,f]} holds
the ResultSort of (1GateCircStr (p,f)) . x = x

let x be object ; :: 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;

A2: the carrier' of (1GateCircStr (p,f)) = {[p,f]} by Def6;
then dom the ResultSort of (1GateCircStr (p,f)) = {[p,f]} by FUNCT_2:def 1;
hence the ResultSort of (1GateCircStr (p,f)) = id the carrier' of (1GateCircStr (p,f)) by A2, A1, FUNCT_1:17; :: 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 A2, 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; :: thesis: verum