let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for F being ManySortedFunction of A,(Trivial_Algebra S)
for o being OperSymbol of S
for x being Element of Args o,A holds
( (F . (the_result_sort_of o)) . ((Den o,A) . x) = 0 & (Den o,(Trivial_Algebra S)) . (F # x) = 0 )
let A be non-empty MSAlgebra of S; :: thesis: for F being ManySortedFunction of A,(Trivial_Algebra S)
for o being OperSymbol of S
for x being Element of Args o,A holds
( (F . (the_result_sort_of o)) . ((Den o,A) . x) = 0 & (Den o,(Trivial_Algebra S)) . (F # x) = 0 )
let F be ManySortedFunction of A,(Trivial_Algebra S); :: thesis: for o being OperSymbol of S
for x being Element of Args o,A holds
( (F . (the_result_sort_of o)) . ((Den o,A) . x) = 0 & (Den o,(Trivial_Algebra S)) . (F # x) = 0 )
let o be OperSymbol of S; :: thesis: for x being Element of Args o,A holds
( (F . (the_result_sort_of o)) . ((Den o,A) . x) = 0 & (Den o,(Trivial_Algebra S)) . (F # x) = 0 )
let x be Element of Args o,A; :: thesis: ( (F . (the_result_sort_of o)) . ((Den o,A) . x) = 0 & (Den o,(Trivial_Algebra S)) . (F # x) = 0 )
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 set 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:150;
reconsider d = (Den o,A) . x as Element of the Sorts of A . (the_result_sort_of o) by FUNCT_2:21;
consider XX being ManySortedSet of the carrier of S such that
A3: {XX} = the carrier of S --> {0 } by Th6;
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, FUNCOP_1:13;
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: (Den o,(Trivial_Algebra S)) . (F # x) = 0
the Sorts of (Trivial_Algebra S) . i = {0 } by A3, A4, A1, FUNCOP_1:13;
hence (Den o,(Trivial_Algebra S)) . (F # x) = 0 by A2, TARSKI:def 1; :: thesis: verum