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 G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G holds (leq (t1,t2)) value_at (C,s) = leq ((t1 value_at (C,s)),(t2 value_at (C,s)))
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 G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G holds (leq (t1,t2)) value_at (C,s) = leq ((t1 value_at (C,s)),(t2 value_at (C,s)))
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 G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G holds (leq (t1,t2)) value_at (C,s) = leq ((t1 value_at (C,s)),(t2 value_at (C,s)))
let C be bool-correct 4,1 integer image of T; for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G holds (leq (t1,t2)) value_at (C,s) = leq ((t1 value_at (C,s)),(t2 value_at (C,s)))
let G be basic GeneratorSystem over S,X,T; for I being integer SortSymbol of S
for t1, t2 being Element of T,I
for s being Element of C -States the generators of G holds (leq (t1,t2)) value_at (C,s) = leq ((t1 value_at (C,s)),(t2 value_at (C,s)))
let I be integer SortSymbol of S; for t1, t2 being Element of T,I
for s being Element of C -States the generators of G holds (leq (t1,t2)) value_at (C,s) = leq ((t1 value_at (C,s)),(t2 value_at (C,s)))
let t1, t2 be Element of T,I; for s being Element of C -States the generators of G holds (leq (t1,t2)) value_at (C,s) = leq ((t1 value_at (C,s)),(t2 value_at (C,s)))
let s be Element of C -States the generators of G; (leq (t1,t2)) value_at (C,s) = leq ((t1 value_at (C,s)),(t2 value_at (C,s)))
A1:
s is ManySortedFunction of the generators of G, the Sorts of C
by AOFA_A00:48;
then consider f being ManySortedFunction of T,C such that
A2:
( f is_homomorphism T,C & s = f || the generators of G )
by AOFA_A00:def 19;
the generators of G is_transformable_to the Sorts of C
by MSAFREE4:21;
then A3:
doms s = the generators of G
by A1, MSSUBFAM:17;
then consider f1 being ManySortedFunction of T,C, Q1 being GeneratorSet of T such that
A4:
( f1 is_homomorphism T,C & Q1 = doms s & s = f1 || Q1 & t1 value_at (C,s) = (f1 . I) . t1 )
by A2, AOFA_A00:def 21;
consider f2 being ManySortedFunction of T,C, Q2 being GeneratorSet of T such that
A5:
( f2 is_homomorphism T,C & Q2 = doms s & s = f2 || Q2 & t2 value_at (C,s) = (f2 . I) . t2 )
by A2, A3, AOFA_A00:def 21;
consider f being ManySortedFunction of T,C, Q being GeneratorSet of T such that
A6:
( f is_homomorphism T,C & Q = doms s & s = f || Q & (leq (t1,t2)) value_at (C,s) = (f . the bool-sort of S) . (leq (t1,t2)) )
by A2, A3, AOFA_A00:def 21;
A7:
( f = f1 & f = f2 )
by A4, A5, A6, EXTENS_1:19;
set o = In (( the connectives of S . 10), the carrier' of S);
A8:
( the_arity_of (In (( the connectives of S . 10), the carrier' of S)) = <*I,I*> & the_result_sort_of (In (( the connectives of S . 10), the carrier' of S)) = the bool-sort of S )
by Th20;
then
Args ((In (( the connectives of S . 10), the carrier' of S)),T) = product <*( the Sorts of T . I),( the Sorts of T . I)*>
by Th23;
then reconsider p = <*t1,t2*> as Element of Args ((In (( the connectives of S . 10), the carrier' of S)),T) by FINSEQ_3:124;
thus (leq (t1,t2)) value_at (C,s) =
(Den ((In (( the connectives of S . 10), the carrier' of S)),C)) . (f # p)
by A6, A8
.=
leq ((t1 value_at (C,s)),(t2 value_at (C,s)))
by A4, A5, A7, A8, Th26
; verum