let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for C being MSCongruence of A
for s being SortSymbol of S
for a being Element of the Sorts of (QuotMSAlg A,C) . s ex x being Element of the Sorts of A . s st a = Class C,x
let A be non-empty MSAlgebra of S; :: thesis: for C being MSCongruence of A
for s being SortSymbol of S
for a being Element of the Sorts of (QuotMSAlg A,C) . s ex x being Element of the Sorts of A . s st a = Class C,x
let C be MSCongruence of A; :: thesis: for s being SortSymbol of S
for a being Element of the Sorts of (QuotMSAlg A,C) . s ex x being Element of the Sorts of A . s st a = Class C,x
let s be SortSymbol of S; :: thesis: for a being Element of the Sorts of (QuotMSAlg A,C) . s ex x being Element of the Sorts of A . s st a = Class C,x
let a be Element of the Sorts of (QuotMSAlg A,C) . s; :: thesis: ex x being Element of the Sorts of A . s st a = Class C,x
a in (Class C) . s ;
then a in Class (C . s) by MSUALG_4:def 8;
then consider t being set such that
A1: t in the Sorts of A . s and
A2: a = Class (C . s),t by EQREL_1:def 5;
reconsider t = t as Element of the Sorts of A . s by A1;
take t ; :: thesis: a = Class C,t
thus a = Class C,t by A2; :: thesis: verum