set S = 1GateCircStr (p,f,x);
let A1, A2 be strict non-empty MSAlgebra over 1GateCircStr (p,f,x); :: thesis: ( the Sorts of A1 = ((rng p) --> X) +* (x .--> Y) & the Charact of A1 . [p,f] = f & the Sorts of A2 = ((rng p) --> X) +* (x .--> Y) & the Charact of A2 . [p,f] = f implies A1 = A2 )
assume A22: ( the Sorts of A1 = ((rng p) --> X) +* (x .--> Y) & the Charact of A1 . [p,f] = f & the Sorts of A2 = ((rng p) --> X) +* (x .--> Y) & the Charact of A2 . [p,f] = f & not A1 = A2 ) ; :: thesis: contradiction
A23: the carrier' of (1GateCircStr (p,f,x)) = {[p,f]} by Def5;
then dom the Charact of A1 = {[p,f]} by PARTFUN1:def 2;
then A24: the Charact of A1 = {[[p,f],f]} by A22, GRFUNC_1:7;
dom the Charact of A2 = {[p,f]} by A23, PARTFUN1:def 2;
hence contradiction by A22, A24, GRFUNC_1:7; :: thesis: verum