thus ex X being MSAlgebra-Class of S, id (Class EqR) st
for c being set st c in Class EqR holds
X . c = A | c :: thesis: verum
proof
deffunc H1( set ) -> set = A | $1;
consider X being ManySortedSet of Class EqR such that
A1: for c being set st c in Class EqR holds
X . c = H1(c) from PBOOLE:sch 7();
 X is MSAlgebra-Class of S, id (Class EqR)
proof
let c be set ; :: according to PRALG_3:def 3 :: thesis: ( c in Class EqR implies X . c is MSAlgebra-Family of (id (Class EqR)) . c,S )
assume A2: c in Class EqR ; :: thesis: X . c is MSAlgebra-Family of (id (Class EqR)) . c,S
A3: dom (A | c) = (dom A) /\ c by RELAT_1:61
.= I /\ c by PARTFUN1:def 2
.= c by A2, XBOOLE_1:28
.= (id (Class EqR)) . c by A2, FUNCT_1:18 ;
then reconsider ac = A | c as ManySortedSet of (id (Class EqR)) . c by PARTFUN1:def 2, RELAT_1:def 18;
ac is MSAlgebra-Family of (id (Class EqR)) . c,S
proof
let i be object ; :: according to PRALG_2:def 5 :: thesis: ( not i in (id (Class EqR)) . c or ac . i is MSAlgebra over S )
assume A4: i in (id (Class EqR)) . c ; :: thesis: ac . i is MSAlgebra over S
dom ac = c by A2, A3, FUNCT_1:18;
then reconsider i9 = i as Element of I by A2, A3, A4;
A . i9 is non-empty MSAlgebra over S ;
hence ac . i is MSAlgebra over S by A3, A4, FUNCT_1:47; :: thesis: verum
end;
hence X . c is MSAlgebra-Family of (id (Class EqR)) . c,S by A1, A2; :: thesis: verum
end;
then reconsider X = X as MSAlgebra-Class of S, id (Class EqR) ;
take X ; :: thesis: for c being set st c in Class EqR holds
X . c = A | c
thus for c being set st c in Class EqR holds
X . c = A | c by A1; :: thesis: verum
end;