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 & 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 over S1; :: thesis: for A2 being non-empty MSAlgebra over 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 over 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) )
A1: dom the Charact of A1 = the carrier' of S1 by PARTFUN1:def 2;
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:15; :: thesis: verum