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 A7: ( 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
the carrier' of (1GateCircStr p,f) = {[p,f]} by Def6;
then ( dom the Charact of A1 = {[p,f]} & dom the Charact of A2 = {[p,f]} ) by PARTFUN1:def 4;
then ( the Charact of A1 = {[[p,f],f]} & the Charact of A2 = {[[p,f],f]} ) by A7, GRFUNC_1:18;
hence contradiction by A7; :: thesis: verum