let I be non empty set ; :: thesis: for M being ManySortedSet of I
for i being Element of I
for e being Equivalence_Relation of (M . i) ex E being Equivalence_Relation of M st
( E . i = e & ( for j being Element of I st j <> i holds
E . j = nabla (M . j) ) )
let M be ManySortedSet of I; :: thesis: for i being Element of I
for e being Equivalence_Relation of (M . i) ex E being Equivalence_Relation of M st
( E . i = e & ( for j being Element of I st j <> i holds
E . j = nabla (M . j) ) )
let i be Element of I; :: thesis: for e being Equivalence_Relation of (M . i) ex E being Equivalence_Relation of M st
( E . i = e & ( for j being Element of I st j <> i holds
E . j = nabla (M . j) ) )
let e be Equivalence_Relation of (M . i); :: thesis: ex E being Equivalence_Relation of M st
( E . i = e & ( for j being Element of I st j <> i holds
E . j = nabla (M . j) ) )
defpred S₁[ object ] means $1 = i;
deffunc H₁( object ) -> Equivalence_Relation of (M . i) = e;
deffunc H₂( object ) -> Element of bool [:(M . $1),(M . $1):] = nabla (M . $1);
consider E being Function such that
A1: dom E = I and
A2: for j being object st j in I holds
( ( S₁[j] implies E . j = H₁(j) ) & ( not S₁[j] implies E . j = H₂(j) ) ) from PARTFUN1:sch 1();
reconsider E = E as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

now :: thesis: for k being set st k in I holds
E . k is Relation of (M . k)

let k be set ; :: thesis: ( k in I implies E . b₁ is Relation of (M . b₁) )
assume A3: k in I ; :: thesis: E . b₁ is Relation of (M . b₁)

per cases ( k = i or k <> i ) ;

suppose k = i ; :: thesis: E . b₁ is Relation of (M . b₁)

hence E . k is Relation of (M . k) by A2; :: thesis: verum

end;

suppose k <> i ; :: thesis: E . b₁ is Relation of (M . b₁)

then E . k = nabla (M . k) by A2, A3;
hence E . k is Relation of (M . k) ; :: thesis: verum

end;

end;

end;

then reconsider E = E as ManySortedRelation of M by MSUALG_4:def 1;

now :: thesis: for k being object
for R being Relation of (M . k) st k in I & E . k = R holds
R is Equivalence_Relation of (M . k)

let k be object ; :: thesis: for R being Relation of (M . k) st k in I & E . k = R holds
b₃ is Equivalence_Relation of (M . b₂)
let R be Relation of (M . k); :: thesis: ( k in I & E . k = R implies b₂ is Equivalence_Relation of (M . b₁) )
assume that
A4: k in I and
A5: E . k = R ; :: thesis: b₂ is Equivalence_Relation of (M . b₁)

per cases ( k = i or k <> i ) ;

suppose k = i ; :: thesis: b₂ is Equivalence_Relation of (M . b₁)

hence R is Equivalence_Relation of (M . k) by A2, A5; :: thesis: verum

end;

suppose k <> i ; :: thesis: b₂ is Equivalence_Relation of (M . b₁)

then E . k = nabla (M . k) by A2, A4;
hence R is Equivalence_Relation of (M . k) by A5; :: thesis: verum

end;

end;

end;

then reconsider E = E as Equivalence_Relation of M by MSUALG_4:def 2;
take E ; :: thesis: ( E . i = e & ( for j being Element of I st j <> i holds
E . j = nabla (M . j) ) )
thus E . i = e by A2; :: thesis: for j being Element of I st j <> i holds
E . j = nabla (M . j)
let j be Element of I; :: thesis: ( j <> i implies E . j = nabla (M . j) )
assume j <> i ; :: thesis: E . j = nabla (M . j)
hence E . j = nabla (M . j) by A2; :: thesis: verum