for X, Y being MSAlgebra-Class of S, id (Class EqR) st ( for c being set st c in Class EqR holds
X . c = A | c ) & ( for c being set st c in Class EqR holds
Y . c = A | c ) holds
X = Y

proof

let X, Y be MSAlgebra-Class of S, id (Class EqR); :: thesis: ( ( for c being set st c in Class EqR holds
X . c = A | c ) & ( for c being set st c in Class EqR holds
Y . c = A | c ) implies X = Y )
assume that
A5: for c being set st c in Class EqR holds
X . c = A | c and
A6: for c being set st c in Class EqR holds
Y . c = A | c ; :: thesis: X = Y

now

let c be set ; :: thesis: ( c in Class EqR implies X . c = Y . c )
assume A7: c in Class EqR ; :: thesis: X . c = Y . c
hence X . c = A | c by A5
.= Y . c by A6, A7 ;
:: thesis: verum

end;

hence X = Y by PBOOLE:3; :: thesis: verum

end;

hence for b₁, b₂ being MSAlgebra-Class of S, id (Class EqR) st ( for c being set st c in Class EqR holds
b₁ . c = A | c ) & ( for c being set st c in Class EqR holds
b₂ . c = A | c ) holds
b₁ = b₂ ; :: thesis: verum