let S1, S2 be non empty ManySortedSign ; for A1 being non-empty finite-yielding MSAlgebra over S1
for A2 being non-empty finite-yielding MSAlgebra over 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 over S1; for A2 being non-empty finite-yielding MSAlgebra over 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 over S2; ( 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
; A1 +* A2 is finite-yielding
let x be object ; FINSET_1:def 5,MSAFREE2:def 11 ( 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 2;
A3:
the Sorts of A1 is V32()
by MSAFREE2:def 11;
assume
x in the carrier of (S1 +* S2)
; 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 2;
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 V32()
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, FUNCT_4:13, FUNCT_4:15;
hence
the Sorts of (A1 +* A2) . x is finite
; verum