let S, T be LATTICE; :: thesis: for f being join-preserving Function of S,T
for S9 being non empty full join-inheriting SubRelStr of S
for T9 being non empty full join-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is join-preserving
let f be join-preserving Function of S,T; :: thesis: for S9 being non empty full join-inheriting SubRelStr of S
for T9 being non empty full join-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is join-preserving
let S9 be non empty full join-inheriting SubRelStr of S; :: thesis: for T9 being non empty full join-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is join-preserving
let T9 be non empty full join-inheriting SubRelStr of T; :: thesis: for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is join-preserving
let g be Function of S9,T9; :: thesis: ( g = f | the carrier of S9 implies g is join-preserving )
assume A1: g = f | the carrier of S9 ; :: thesis: g is join-preserving
now :: thesis: for x, y being Element of S9 holds g . (x "\/" y) = (g . x) "\/" (g . y)
let x, y be Element of S9; :: thesis: g . (x "\/" y) = (g . x) "\/" (g . y)
reconsider a = x, b = y as Element of S by YELLOW_0:58;
x "\/" y = a "\/" b by YELLOW_0:70;
then A2: g . (x "\/" y) = f . (a "\/" b) by A1, FUNCT_1:49;
A3: g . x = f . a by A1, FUNCT_1:49;
A4: g . y = f . b by A1, FUNCT_1:49;
thus g . (x "\/" y) = (f . a) "\/" (f . b) by A2, WAYBEL_6:2
.= (g . x) "\/" (g . y) by A3, A4, YELLOW_0:70 ; :: thesis: verum
end;
hence g is join-preserving by WAYBEL_6:2; :: thesis: verum