let A1, A2 be strict non-empty MSAlgebra over S; :: thesis: ( the Sorts of A1 = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,A1) holds (Den (o,A1)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) & the Sorts of A2 = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,A2) holds (Den (o,A2)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) implies A1 = A2 )
assume that
A5: ( the Sorts of A1 = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,A1) holds (Den (o,A1)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) ) and
A6: ( the Sorts of A2 = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,A2) holds (Den (o,A2)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) ) ; :: thesis: A1 = A2
the Charact of A1 = the Charact of A2

proof

let o be OperSymbol of S; :: according to PBOOLE:def 21 :: thesis: the Charact of A1 . o = the Charact of A2 . o
A7: ( dom (Den (o,A1)) = Args (o,A1) & dom (Den (o,A2)) = Args (o,A2) ) by FUNCT_2:def 1;

now :: thesis: for a being object st a in Args (o,A1) holds
(Den (o,A1)) . a = (Den (o,A2)) . a

let a be object ; :: thesis: ( a in Args (o,A1) implies (Den (o,A1)) . a = (Den (o,A2)) . a )
assume a in Args (o,A1) ; :: thesis: (Den (o,A1)) . a = (Den (o,A2)) . a
then ( (Den (o,A1)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) & (Den (o,A2)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) by A5, A6;
hence (Den (o,A1)) . a = (Den (o,A2)) . a ; :: thesis: verum

end;

hence the Charact of A1 . o = the Charact of A2 . o by A5, A6, A7, FUNCT_1:2; :: thesis: verum

end;

hence A1 = A2 by A5, A6; :: thesis: verum