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: ( bind B,j,k = B . k,j & bind B,i,j = B . j,i & bind B,i,k = B . k,i ) by Def3, ORDERS_2:26;
consider f1 being ManySortedFunction of (OAF . i),(OAF . j), f2 being ManySortedFunction of (OAF . j),(OAF . k) such that
A3: ( f1 = B . j,i & f2 = B . k,j & B . k,i = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by A1, Def2;
thus (bind B,j,k) ** (bind B,i,j) = bind B,i,k by A2, A3; :: thesis: verum