let S1, S2 be non empty ManySortedSign ; :: thesis: for A1 being non-empty finite-yielding MSAlgebra of S1
for A2 being non-empty finite-yielding MSAlgebra of S2 st the Sorts of A1 tolerates the Sorts of A2 holds
A1 +* A2 is finite-yielding
let A1 be non-empty finite-yielding MSAlgebra of S1; :: thesis: for A2 being non-empty finite-yielding MSAlgebra of S2 st the Sorts of A1 tolerates the Sorts of A2 holds
A1 +* A2 is finite-yielding
let A2 be non-empty finite-yielding MSAlgebra of S2; :: thesis: ( the Sorts of A1 tolerates the Sorts of A2 implies A1 +* A2 is finite-yielding )
assume A1: the Sorts of A1 tolerates the Sorts of A2 ; :: thesis: A1 +* A2 is finite-yielding
let x be set ; :: according to FINSET_1:def 4,MSAFREE2:def 11 :: thesis: ( not x in the carrier of (S1 +* S2) or the Sorts of (A1 +* A2) . x is finite )
set A = A1 +* A2;
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 = the carrier of S1 by PARTFUN1:def 4;
A3: the Sorts of A1 is finite-yielding by MSAFREE2:def 11;
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) ;
A4: dom the Sorts of A2 = the carrier of S2 by PARTFUN1:def 4;
the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by Def2;
then A5: ( x in the carrier of S1 or x in the carrier of S2 ) by XBOOLE_0:def 3;
A6: the Sorts of A2 is finite-yielding by MSAFREE2:def 11;
the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by A1, Def4;
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, A4, A5, A3, A6, FINSET_1:def 4, FUNCT_4:14, FUNCT_4:16;
hence the Sorts of (A1 +* A2) . x is finite ; :: thesis: verum