let P be non empty Poset; :: thesis: for i, j, k being Element of P
for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF st i >= j & j >= k holds
(bind B,j,k) ** (bind B,i,j) = bind B,i,k
let i, j, k be Element of P; :: thesis: for S being non empty non void ManySortedSign
for OAF being OrderedAlgFam of P,S
for B being Binding of OAF st i >= j & j >= k holds
(bind B,j,k) ** (bind B,i,j) = bind B,i,k
let S be non empty non void ManySortedSign ; :: thesis: for OAF being OrderedAlgFam of P,S
for B being Binding of OAF st i >= j & j >= k holds
(bind B,j,k) ** (bind B,i,j) = bind B,i,k
let OAF be OrderedAlgFam of P,S; :: thesis: for B being Binding of OAF st i >= j & j >= k holds
(bind B,j,k) ** (bind B,i,j) = bind B,i,k
let B be Binding of OAF; :: thesis: ( i >= j & j >= k implies (bind B,j,k) ** (bind B,i,j) = bind B,i,k )
assume A1: ( i >= j & j >= k ) ; :: thesis: (bind B,j,k) ** (bind B,i,j) = bind B,i,k
then A2: ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . k) st
( f1 = B . j,i & f2 = B . k,j & B . k,i = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by Def2;
( bind B,j,k = B . k,j & bind B,i,j = B . j,i ) by A1, Def3;
hence (bind B,j,k) ** (bind B,i,j) = bind B,i,k by A1, A2, Def3, ORDERS_2:26; :: thesis: verum