let S1, S2 be non empty non void ManySortedSign ; :: thesis: for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over 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 over S1; :: thesis: for A2 being non-empty MSAlgebra over 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 over 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) )
A1: dom the Charact of A2 = the carrier' of S2 by PARTFUN1:def 2;
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:13; :: thesis: verum