set S = 1GateCircStr p,f;
let A1, A2 be strict non-empty MSAlgebra of 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 4;
then A16: the Charact of A1 = {[[p,f],f]} by A14, GRFUNC_1:18;
dom the Charact of A2 = {[p,f]} by A15, PARTFUN1:def 4;
hence contradiction by A14, A16, GRFUNC_1:18; :: thesis: verum