let S1, S2 be non void strict ManySortedSign ; :: thesis: ( the carrier of S1 = (rng p) \/ {[p,f]} & the carrier' of S1 = {[p,f]} & the Arity of S1 . [p,f] = p & the ResultSort of S1 . [p,f] = [p,f] & the carrier of S2 = (rng p) \/ {[p,f]} & the carrier' of S2 = {[p,f]} & the Arity of S2 . [p,f] = p & the ResultSort of S2 . [p,f] = [p,f] implies S1 = S2 )
assume A1: ( the carrier of S1 = (rng p) \/ {[p,f]} & the carrier' of S1 = {[p,f]} & the Arity of S1 . [p,f] = p & the ResultSort of S1 . [p,f] = [p,f] & the carrier of S2 = (rng p) \/ {[p,f]} & the carrier' of S2 = {[p,f]} & the Arity of S2 . [p,f] = p & the ResultSort of S2 . [p,f] = [p,f] & not S1 = S2 ) ; :: thesis: contradiction
then S1 = 1GateCircStr (p,f,[p,f]) by Def5;
hence contradiction by A1, Def5; :: thesis: verum