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