set S = 1GateCircStr (p,f);
let A1, A2 be strict non-empty MSAlgebra over 1GateCircStr (p,f); :: thesis: ( the Sorts of A1 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of A1 . [p,f] = f & the Sorts of A2 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of A2 . [p,f] = f implies A1 = A2 )
assume A14: ( the Sorts of A1 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of A1 . [p,f] = f & the Sorts of A2 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of A2 . [p,f] = f & not A1 = A2 ) ; :: thesis: contradiction
A15: the carrier' of (1GateCircStr (p,f)) = {[p,f]} by Def6;
then dom the Charact of A1 = {[p,f]} by PARTFUN1:def 2;
then A16: the Charact of A1 = {[[p,f],f]} by A14, GRFUNC_1:7;
dom the Charact of A2 = {[p,f]} by A15, PARTFUN1:def 2;
hence contradiction by A14, A16, GRFUNC_1:7; :: thesis: verum