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