set f = the set ;
set p = the FinSequence;
take
1GateCircStr ( the FinSequence, the set )
; ( 1GateCircStr ( the FinSequence, the set ) is unsplit & 1GateCircStr ( the FinSequence, the set ) is gate`1=arity & not 1GateCircStr ( the FinSequence, the set ) is void & 1GateCircStr ( the FinSequence, the set ) is strict & not 1GateCircStr ( the FinSequence, the set ) is empty )
thus
( 1GateCircStr ( the FinSequence, the set ) is unsplit & 1GateCircStr ( the FinSequence, the set ) is gate`1=arity & not 1GateCircStr ( the FinSequence, the set ) is void & 1GateCircStr ( the FinSequence, the set ) is strict & not 1GateCircStr ( the FinSequence, the set ) is empty )
; verum