set f = the set ;
set p = the FinSequence;
take 1GateCircStr ( the FinSequence, the set ) ; :: thesis: ( 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 ) ; :: thesis: verum