let S be non void Signature; :: thesis: for A being disjoint_valued MSAlgebra over S
for C1, C2 being Component of the Sorts of A holds
( C1 = C2 or C1 misses C2 )
let A be disjoint_valued MSAlgebra over S; :: thesis: for C1, C2 being Component of the Sorts of A holds
( C1 = C2 or C1 misses C2 )
let C1, C2 be Component of the Sorts of A; :: thesis: ( C1 = C2 or C1 misses C2 )
A1: ex y being object st
( y in dom the Sorts of A & C2 = the Sorts of A . y ) by FUNCT_1:def 3;
A2: the Sorts of A is disjoint_valued by MSAFREE1:def 2;
ex x being object st
( x in dom the Sorts of A & C1 = the Sorts of A . x ) by FUNCT_1:def 3;
hence ( C1 = C2 or C1 misses C2 ) by A1, A2, PROB_2:def 2; :: thesis: verum