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 holds
for o being OperSymbol of (S1 +* S2)
for o2 being OperSymbol of S2 st o = o2 holds
Den o,(A1 +* A2) = Den o2,A2
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 holds
for o being OperSymbol of (S1 +* S2)
for o2 being OperSymbol of S2 st o = o2 holds
Den o,(A1 +* A2) = Den o2,A2
let A2 be non-empty MSAlgebra of S2; :: thesis: ( the Sorts of A1 tolerates the Sorts of A2 implies for o being OperSymbol of (S1 +* S2)
for o2 being OperSymbol of S2 st o = o2 holds
Den o,(A1 +* A2) = Den o2,A2 )
set A = A1 +* A2;
A1: dom the Charact of A2 = the carrier' of S2 by PARTFUN1:def 4;
assume the Sorts of A1 tolerates the Sorts of A2 ; :: thesis: for o being OperSymbol of (S1 +* S2)
for o2 being OperSymbol of S2 st o = o2 holds
Den o,(A1 +* A2) = Den o2,A2
then A2: the Charact of (A1 +* A2) = the Charact of A1 +* the Charact of A2 by Def4;
let o be OperSymbol of (S1 +* S2); :: thesis: for o2 being OperSymbol of S2 st o = o2 holds
Den o,(A1 +* A2) = Den o2,A2
let o2 be OperSymbol of S2; :: thesis: ( o = o2 implies Den o,(A1 +* A2) = Den o2,A2 )
assume o = o2 ; :: thesis: Den o,(A1 +* A2) = Den o2,A2
hence Den o,(A1 +* A2) = Den o2,A2 by A2, A1, FUNCT_4:14; :: thesis: verum