take 1GateCircStr p,f,[p,f] ; :: thesis: ( the carrier of (1GateCircStr p,f,[p,f]) = (rng p) \/ {[p,f]} & the carrier' of (1GateCircStr p,f,[p,f]) = {[p,f]} & the Arity of (1GateCircStr p,f,[p,f]) . [p,f] = p & the ResultSort of (1GateCircStr p,f,[p,f]) . [p,f] = [p,f] )
thus ( the carrier of (1GateCircStr p,f,[p,f]) = (rng p) \/ {[p,f]} & the carrier' of (1GateCircStr p,f,[p,f]) = {[p,f]} & the Arity of (1GateCircStr p,f,[p,f]) . [p,f] = p & the ResultSort of (1GateCircStr p,f,[p,f]) . [p,f] = [p,f] ) by Def5; :: thesis: verum