let S be non empty non void bool-correct 4,1 integer BoolSignature ; for X being V3() ManySortedSet of the carrier of S
for T being b1,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for I being integer SortSymbol of S
for t being Element of T,I
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (- t) value_at (C,u) = - (t value_at (C,u))
let X be V3() ManySortedSet of the carrier of S; for T being X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for I being integer SortSymbol of S
for t being Element of T,I
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (- t) value_at (C,u) = - (t value_at (C,u))
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; for C being bool-correct 4,1 integer image of T
for I being integer SortSymbol of S
for t being Element of T,I
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (- t) value_at (C,u) = - (t value_at (C,u))
let C be bool-correct 4,1 integer image of T; for I being integer SortSymbol of S
for t being Element of T,I
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (- t) value_at (C,u) = - (t value_at (C,u))
let I be integer SortSymbol of S; for t being Element of T,I
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (- t) value_at (C,u) = - (t value_at (C,u))
let t be Element of T,I; for u being ManySortedFunction of FreeGen T, the Sorts of C holds (- t) value_at (C,u) = - (t value_at (C,u))
let u be ManySortedFunction of FreeGen T, the Sorts of C; (- t) value_at (C,u) = - (t value_at (C,u))
consider f being ManySortedFunction of T,C such that
A1:
( f is_homomorphism T,C & u = f || (FreeGen T) )
by MSAFREE4:46;
FreeGen T is_transformable_to the Sorts of C
by MSAFREE4:21;
then A2:
doms u = FreeGen T
by MSSUBFAM:17;
then consider f1 being ManySortedFunction of T,C, Q1 being GeneratorSet of T such that
A3:
( f1 is_homomorphism T,C & Q1 = doms u & u = f1 || Q1 & t value_at (C,u) = (f1 . I) . t )
by A1, AOFA_A00:def 21;
consider f2 being ManySortedFunction of T,C, Q2 being GeneratorSet of T such that
A4:
( f2 is_homomorphism T,C & Q2 = doms u & u = f2 || Q2 & (- t) value_at (C,u) = (f2 . I) . (- t) )
by A1, A2, AOFA_A00:def 21;
set o = In (( the connectives of S . 6), the carrier' of S);
A5:
( the_arity_of (In (( the connectives of S . 6), the carrier' of S)) = <*I*> & the_result_sort_of (In (( the connectives of S . 6), the carrier' of S)) = I )
by Th16;
then
Args ((In (( the connectives of S . 6), the carrier' of S)),T) = product <*( the Sorts of T . I)*>
by Th22;
then reconsider p = <*t*> as Element of Args ((In (( the connectives of S . 6), the carrier' of S)),T) by FINSEQ_3:123;
thus (- t) value_at (C,u) =
(Den ((In (( the connectives of S . 6), the carrier' of S)),C)) . (f2 # p)
by A4, A5
.=
(Den ((In (( the connectives of S . 6), the carrier' of S)),C)) . <*((f2 . I) . t)*>
by A5, Th25
.=
- (t value_at (C,u))
by A3, A4, EXTENS_1:19
; verum