let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for C1, C2 being MSCongruence of A holds C1 (/\) C2 is MSCongruence of A
let A be non-empty MSAlgebra over S; :: thesis: for C1, C2 being MSCongruence of A holds C1 (/\) C2 is MSCongruence of A
let C1, C2 be MSCongruence of A; :: thesis: C1 (/\) C2 is MSCongruence of A
reconsider C = C1 (/\) C2 as Equivalence_Relation of the Sorts of A by Th11;
reconsider C = C as MSEquivalence_Relation-like ManySortedRelation of the Sorts of A ;
reconsider C = C as ManySortedRelation of A ;
reconsider C = C as MSEquivalence-like ManySortedRelation of A by MSUALG_4:def 3;
for o being OperSymbol of S
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)

proof

let o be OperSymbol of S; :: thesis: for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
let x, y be Element of Args (o,A); :: thesis: ( ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) implies [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) )
assume A1: for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ; :: thesis: [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)
for n being Nat st n in dom x holds
[(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)

proof

let n be Nat; :: thesis: ( n in dom x implies [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) )
assume n in dom x ; :: thesis: [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n)
then [(x . n),(y . n)] in C . ((the_arity_of o) /. n) by A1;
then [(x . n),(y . n)] in (C1 . ((the_arity_of o) /. n)) /\ (C2 . ((the_arity_of o) /. n)) by PBOOLE:def 5;
hence [(x . n),(y . n)] in C1 . ((the_arity_of o) /. n) by XBOOLE_0:def 4; :: thesis: verum

end;

then A2: [((Den (o,A)) . x),((Den (o,A)) . y)] in C1 . (the_result_sort_of o) by MSUALG_4:def 4;
for n being Nat st n in dom x holds
[(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)

proof

let n be Nat; :: thesis: ( n in dom x implies [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) )
assume n in dom x ; :: thesis: [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n)
then [(x . n),(y . n)] in C . ((the_arity_of o) /. n) by A1;
then [(x . n),(y . n)] in (C1 . ((the_arity_of o) /. n)) /\ (C2 . ((the_arity_of o) /. n)) by PBOOLE:def 5;
hence [(x . n),(y . n)] in C2 . ((the_arity_of o) /. n) by XBOOLE_0:def 4; :: thesis: verum

end;

then A3: [((Den (o,A)) . x),((Den (o,A)) . y)] in C2 . (the_result_sort_of o) by MSUALG_4:def 4;
(C1 . (the_result_sort_of o)) /\ (C2 . (the_result_sort_of o)) = C . (the_result_sort_of o) by PBOOLE:def 5;
hence [((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o) by A2, A3, XBOOLE_0:def 4; :: thesis: verum

end;

hence C1 (/\) C2 is MSCongruence of A by MSUALG_4:def 4; :: thesis: verum