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:3; :: thesis: verum