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 S1[ object ] means $1 = i;
deffunc H1( object ) -> Equivalence_Relation of (M . i) = e;
deffunc H2( 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
( ( S1[j] implies E . j = H1(j) ) & ( not S1[j] implies E . j = H2(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 . b1 is Relation of (M . b1) )
assume A3: k in I ; :: thesis: E . b1 is Relation of (M . b1)
per cases ( k = i or k <> i ) ;
suppose k = i ; :: thesis: E . b1 is Relation of (M . b1)
hence E . k is Relation of (M . k) by A2; :: thesis: verum
end;
suppose k <> i ; :: thesis: E . b1 is Relation of (M . b1)
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 set
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 set ; :: thesis: for R being Relation of (M . k) st k in I & E . k = R holds
b3 is Equivalence_Relation of (M . b2)
let R be Relation of (M . k); :: thesis: ( k in I & E . k = R implies b2 is Equivalence_Relation of (M . b1) )
assume that
A4: k in I and
A5: E . k = R ; :: thesis: b2 is Equivalence_Relation of (M . b1)
per cases ( k = i or k <> i ) ;
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