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);
consider XX being ManySortedSet of such that
A1: {XX} = the carrier of S --> {0 } by Th6;
A2: the Sorts of (Trivial_Algebra S) = {XX} by A1, MSAFREE2:def 12;
set r = the_result_sort_of o;
consider i being set such that
A3: i in the carrier of S and
A4: Result o,(Trivial_Algebra S) = the Sorts of (Trivial_Algebra S) . i by PBOOLE:150;
A5: the Sorts of (Trivial_Algebra S) . i = {0 } by A1, A2, A3, FUNCOP_1:13;
reconsider d = (Den o,A) . x as Element of the Sorts of A . (the_result_sort_of o) by FUNCT_2:21;
A6: the Sorts of (Trivial_Algebra S) . (the_result_sort_of o) = {0 } by A1, A2, FUNCOP_1:13;
thus (F . (the_result_sort_of o)) . ((Den o,A) . x) = (F . (the_result_sort_of o)) . d
.= 0 by A6, TARSKI:def 1 ; :: thesis: (Den o,(Trivial_Algebra S)) . (F # x) = 0
thus (Den o,(Trivial_Algebra S)) . (F # x) = 0 by A4, A5, TARSKI:def 1; :: thesis: verum