let S1, S2 be non empty ManySortedSign ; :: thesis: for A1 being non-empty locally-finite MSAlgebra of S1
for A2 being non-empty locally-finite MSAlgebra of S2 st the Sorts of A1 tolerates the Sorts of A2 holds
A1 +* A2 is locally-finite
let A1 be non-empty locally-finite MSAlgebra of S1; :: thesis: for A2 being non-empty locally-finite MSAlgebra of S2 st the Sorts of A1 tolerates the Sorts of A2 holds
A1 +* A2 is locally-finite
let A2 be non-empty locally-finite MSAlgebra of S2; :: thesis: ( the Sorts of A1 tolerates the Sorts of A2 implies A1 +* A2 is locally-finite )
assume A1: the Sorts of A1 tolerates the Sorts of A2 ; :: thesis: A1 +* A2 is locally-finite
set A = A1 +* A2;
let x be set ; :: according to PRE_CIRC:def 3,MSAFREE2:def 11 :: thesis: ( not x in the carrier of (S1 +* S2) or the Sorts of (A1 +* A2) . x is finite )
assume x in the carrier of (S1 +* S2) ; :: thesis: the Sorts of (A1 +* A2) . x is finite
then reconsider x = x as Vertex of (S1 +* S2) ;
set SA = the Sorts of (A1 +* A2);
set SA1 = the Sorts of A1;
set SA2 = the Sorts of A2;
A2: ( dom the Sorts of (A1 +* A2) = the carrier of (S1 +* S2) & dom the Sorts of A1 = the carrier of S1 & dom the Sorts of A2 = the carrier of S2 ) by PBOOLE:def 3;
the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by Def2;
then A3: ( x in the carrier of S1 or x in the carrier of S2 ) by XBOOLE_0:def 3;
( the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 & the Sorts of A1 is locally-finite & the Sorts of A2 is locally-finite ) by A1, Def4, MSAFREE2:def 11;
then ( ( the Sorts of (A1 +* A2) . x = the Sorts of A1 . x & the Sorts of A1 . x is finite ) or ( the Sorts of (A1 +* A2) . x = the Sorts of A2 . x & the Sorts of A2 . x is finite ) ) by A1, A2, A3, FUNCT_4:14, FUNCT_4:16, PRE_CIRC:def 3;
hence the Sorts of (A1 +* A2) . x is finite ; :: thesis: verum