let i be object ; :: according to FINSET_1:def 5,MSAFREE2:def 11 :: thesis: ( not i in the carrier of (1GateCircStr (p,f)) or the Sorts of (1GateCircuit (p,f)) . i is finite )
set S = 1GateCircStr (p,f);
assume i in the carrier of (1GateCircStr (p,f)) ; :: thesis: the Sorts of (1GateCircuit (p,f)) . i is finite
hence the Sorts of (1GateCircuit (p,f)) . i is finite by Th54; :: thesis: verum