let S, T be LATTICE; :: thesis: for f being join-preserving Function of S,T
for S' being non empty full join-inheriting SubRelStr of S
for T' being non empty full join-inheriting SubRelStr of T
for g being Function of S',T' st g = f | the carrier of S' holds
g is join-preserving
let f be join-preserving Function of S,T; :: thesis: for S' being non empty full join-inheriting SubRelStr of S
for T' being non empty full join-inheriting SubRelStr of T
for g being Function of S',T' st g = f | the carrier of S' holds
g is join-preserving
let S' be non empty full join-inheriting SubRelStr of S; :: thesis: for T' being non empty full join-inheriting SubRelStr of T
for g being Function of S',T' st g = f | the carrier of S' holds
g is join-preserving
let T' be non empty full join-inheriting SubRelStr of T; :: thesis: for g being Function of S',T' st g = f | the carrier of S' holds
g is join-preserving
let g be Function of S',T'; :: thesis: ( g = f | the carrier of S' implies g is join-preserving )
assume A1: g = f | the carrier of S' ; :: thesis: g is join-preserving

now

let x, y be Element of S'; :: thesis: g . (x "\/" y) = (g . x) "\/" (g . y)
reconsider a = x, b = y as Element of S by YELLOW_0:59;
( x "\/" y = a "\/" b & x in the carrier of S' & a in the carrier of S & the carrier of T <> {} ) by YELLOW_0:71;
then A2: ( g . (x "\/" y) = f . (a "\/" b) & g . x = f . a & g . y = f . b ) by A1, FUNCT_1:72;
hence g . (x "\/" y) = (f . a) "\/" (f . b) by WAYBEL_6:2
.= (g . x) "\/" (g . y) by A2, YELLOW_0:71 ;
:: thesis: verum

end;

hence g is join-preserving by WAYBEL_6:2; :: thesis: verum