let S1, S2 be non empty ManySortedSign ; :: thesis: for A1 being non-empty MSAlgebra over S1
for s1 being Element of product the Sorts of A1
for A2 being non-empty MSAlgebra over S2
for s2 being Element of product the Sorts of A2 st the Sorts of A1 tolerates the Sorts of A2 holds
s1 +* s2 in product the Sorts of (A1 +* A2)
let A1 be non-empty MSAlgebra over S1; :: thesis: for s1 being Element of product the Sorts of A1
for A2 being non-empty MSAlgebra over S2
for s2 being Element of product the Sorts of A2 st the Sorts of A1 tolerates the Sorts of A2 holds
s1 +* s2 in product the Sorts of (A1 +* A2)
let s1 be Element of product the Sorts of A1; :: thesis: for A2 being non-empty MSAlgebra over S2
for s2 being Element of product the Sorts of A2 st the Sorts of A1 tolerates the Sorts of A2 holds
s1 +* s2 in product the Sorts of (A1 +* A2)
let A2 be non-empty MSAlgebra over S2; :: thesis: for s2 being Element of product the Sorts of A2 st the Sorts of A1 tolerates the Sorts of A2 holds
s1 +* s2 in product the Sorts of (A1 +* A2)
let s2 be Element of product the Sorts of A2; :: thesis: ( the Sorts of A1 tolerates the Sorts of A2 implies s1 +* s2 in product the Sorts of (A1 +* A2) )
assume the Sorts of A1 tolerates the Sorts of A2 ; :: thesis: s1 +* s2 in product the Sorts of (A1 +* A2)
then the Sorts of (A1 +* A2) = the Sorts of A1 +* the Sorts of A2 by Def4;
hence s1 +* s2 in product the Sorts of (A1 +* A2) by CARD_3:97; :: thesis: verum