let S be non empty non void ManySortedSign ; :: thesis:
let A be non-empty MSAlgebra over S; :: thesis:
let F be ManySortedFunction of A,(Trivial_Algebra S); :: thesis:
let o be OperSymbol of S; :: thesis:
let x be Element of Args (o,A); :: thesis:
set I = the carrier of S;
set SA = the Sorts of A;
set T = Trivial_Algebra S;
set ST = the Sorts of (Trivial_Algebra S);
set r = the_result_sort_of o;
consider i being object such that
A1: i in the carrier of S and
A2: Result (o,(Trivial_Algebra S)) = the Sorts of (Trivial_Algebra S) . i by PBOOLE:138;
reconsider d = (Den (o,A)) . x as Element of the Sorts of A . (the_result_sort_of o) by FUNCT_2:15;
consider XX being ManySortedSet of the carrier of S such that
A3: {XX} = the carrier of S --> {0} by Th5;
A4: the Sorts of (Trivial_Algebra S) = {XX} by A3, MSAFREE2:def 12;
then A5: the Sorts of (Trivial_Algebra S) . (the_result_sort_of o) = {0} by A3;
thus (F . (the_result_sort_of o)) . ((Den (o,A)) . x) = (F . (the_result_sort_of o)) . d
.= 0 by A5, TARSKI:def 1 ; :: thesis:
the Sorts of (Trivial_Algebra S) . i = {0} by A3, A4, A1, FUNCOP_1:7;
hence (Den (o,(Trivial_Algebra S))) . (F # x) = 0 by A2, TARSKI:def 1; :: thesis: