let P be non empty Poset; 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 ; 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; 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; 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; ( 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
; 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); ( f = bind (B,i,j) implies f is_homomorphism OAF . i,OAF . j )
assume A2:
f = bind (B,i,j)
; 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; verum