let P be non empty Poset; :: thesis: for S being non empty non void ManySortedSign

for OAF being OrderedAlgFam of P,S

for B being Binding of OAF

for i, j being Element of P st i >= j holds

for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j

let S be non empty non void ManySortedSign ; :: thesis: for OAF being OrderedAlgFam of P,S

for B being Binding of OAF

for i, j being Element of P st i >= j holds

for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j

let OAF be OrderedAlgFam of P,S; :: thesis: for B being Binding of OAF

for i, j being Element of P st i >= j holds

for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j

let B be Binding of OAF; :: thesis: for i, j being Element of P st i >= j holds

for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j

let i, j be Element of P; :: thesis: ( i >= j implies for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j )

assume A1: i >= j ; :: thesis: for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j

let f be ManySortedFunction of (OAF . i),(OAF . j); :: thesis: ( f = bind (B,i,j) implies f is_homomorphism OAF . i,OAF . j )

assume A2: f = bind (B,i,j) ; :: thesis: f is_homomorphism OAF . i,OAF . j

j >= j by ORDERS_2:1;

then ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . j) st

( f1 = B . (j,i) & f2 = B . (j,j) & B . (j,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by A1, Def2;

hence f is_homomorphism OAF . i,OAF . j by A1, A2, Def3; :: thesis: verum

for OAF being OrderedAlgFam of P,S

for B being Binding of OAF

for i, j being Element of P st i >= j holds

for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j

let S be non empty non void ManySortedSign ; :: thesis: for OAF being OrderedAlgFam of P,S

for B being Binding of OAF

for i, j being Element of P st i >= j holds

for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j

let OAF be OrderedAlgFam of P,S; :: thesis: for B being Binding of OAF

for i, j being Element of P st i >= j holds

for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j

let B be Binding of OAF; :: thesis: for i, j being Element of P st i >= j holds

for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j

let i, j be Element of P; :: thesis: ( i >= j implies for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j )

assume A1: i >= j ; :: thesis: for f being ManySortedFunction of (OAF . i),(OAF . j) st f = bind (B,i,j) holds

f is_homomorphism OAF . i,OAF . j

let f be ManySortedFunction of (OAF . i),(OAF . j); :: thesis: ( f = bind (B,i,j) implies f is_homomorphism OAF . i,OAF . j )

assume A2: f = bind (B,i,j) ; :: thesis: f is_homomorphism OAF . i,OAF . j

j >= j by ORDERS_2:1;

then ex f1 being ManySortedFunction of (OAF . i),(OAF . j) ex f2 being ManySortedFunction of (OAF . j),(OAF . j) st

( f1 = B . (j,i) & f2 = B . (j,j) & B . (j,i) = f2 ** f1 & f1 is_homomorphism OAF . i,OAF . j ) by A1, Def2;

hence f is_homomorphism OAF . i,OAF . j by A1, A2, Def3; :: thesis: verum