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

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