let I be non empty set ; :: thesis: for M being ManySortedSet of I holds [|M,M|] is Equivalence_Relation of M

let M be ManySortedSet of I; :: thesis: [|M,M|] is Equivalence_Relation of M

set J = [|M,M|];

for i being set st i in I holds

[|M,M|] . i is Relation of (M . i)

for i being set

for R being Relation of (M . i) st i in I & J . i = R holds

R is Equivalence_Relation of (M . i)

let M be ManySortedSet of I; :: thesis: [|M,M|] is Equivalence_Relation of M

set J = [|M,M|];

for i being set st i in I holds

[|M,M|] . i is Relation of (M . i)

proof

then reconsider J = [|M,M|] as ManySortedRelation of M by MSUALG_4:def 1;
let i be set ; :: thesis: ( i in I implies [|M,M|] . i is Relation of (M . i) )

assume i in I ; :: thesis: [|M,M|] . i is Relation of (M . i)

then [|M,M|] . i c= [:(M . i),(M . i):] by PBOOLE:def 16;

hence [|M,M|] . i is Relation of (M . i) ; :: thesis: verum

end;assume i in I ; :: thesis: [|M,M|] . i is Relation of (M . i)

then [|M,M|] . i c= [:(M . i),(M . i):] by PBOOLE:def 16;

hence [|M,M|] . i is Relation of (M . i) ; :: thesis: verum

for i being set

for R being Relation of (M . i) st i in I & J . i = R holds

R is Equivalence_Relation of (M . i)

proof

hence
[|M,M|] is Equivalence_Relation of M
by MSUALG_4:def 2; :: thesis: verum
let i be set ; :: thesis: for R being Relation of (M . i) st i in I & J . i = R holds

R is Equivalence_Relation of (M . i)

let R be Relation of (M . i); :: thesis: ( i in I & J . i = R implies R is Equivalence_Relation of (M . i) )

assume that

A1: i in I and

A2: J . i = R ; :: thesis: R is Equivalence_Relation of (M . i)

J . i = [:(M . i),(M . i):] by A1, PBOOLE:def 16

.= nabla (M . i) by EQREL_1:def 1 ;

hence R is Equivalence_Relation of (M . i) by A2, EQREL_1:4; :: thesis: verum

end;R is Equivalence_Relation of (M . i)

let R be Relation of (M . i); :: thesis: ( i in I & J . i = R implies R is Equivalence_Relation of (M . i) )

assume that

A1: i in I and

A2: J . i = R ; :: thesis: R is Equivalence_Relation of (M . i)

J . i = [:(M . i),(M . i):] by A1, PBOOLE:def 16

.= nabla (M . i) by EQREL_1:def 1 ;

hence R is Equivalence_Relation of (M . i) by A2, EQREL_1:4; :: thesis: verum