let S1, S2 be non empty non void ManySortedSign ; :: thesis: for A1 being non-empty MSAlgebra of S1
for A2 being non-empty MSAlgebra of S2 st the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 holds
for o being OperSymbol of (S1 +* S2)
for o1 being OperSymbol of S1 st o = o1 holds
Den o,(A1 +* A2) = Den o1,A1
let A1 be non-empty MSAlgebra of S1; :: thesis: for A2 being non-empty MSAlgebra of S2 st the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 holds
for o being OperSymbol of (S1 +* S2)
for o1 being OperSymbol of S1 st o = o1 holds
Den o,(A1 +* A2) = Den o1,A1
let A2 be non-empty MSAlgebra of S2; :: thesis: ( the Sorts of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2 implies for o being OperSymbol of (S1 +* S2)
for o1 being OperSymbol of S1 st o = o1 holds
Den o,(A1 +* A2) = Den o1,A1 )
set A = A1 +* A2;
A1: dom the Charact of A1 = the carrier' of S1 by PARTFUN1:def 4;
assume the Sorts of A1 tolerates the Sorts of A2 ; :: thesis: ( not the Charact of A1 tolerates the Charact of A2 or for o being OperSymbol of (S1 +* S2)
for o1 being OperSymbol of S1 st o = o1 holds
Den o,(A1 +* A2) = Den o1,A1 )
then A2: the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2 by Def4;
assume A3: the Charact of A1 tolerates the Charact of A2 ; :: thesis: for o being OperSymbol of (S1 +* S2)
for o1 being OperSymbol of S1 st o = o1 holds
Den o,(A1 +* A2) = Den o1,A1
let o be OperSymbol of (S1 +* S2); :: thesis: for o1 being OperSymbol of S1 st o = o1 holds
Den o,(A1 +* A2) = Den o1,A1
let o1 be OperSymbol of S1; :: thesis: ( o = o1 implies Den o,(A1 +* A2) = Den o1,A1 )
assume o = o1 ; :: thesis: Den o,(A1 +* A2) = Den o1,A1
hence Den o,(A1 +* A2) = Den o1,A1 by A2, A3, A1, FUNCT_4:16; :: thesis: verum