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