let S, T be lower-bounded LATTICE; :: thesis: for f being finite-sups-preserving Function of S,T
for S9 being non empty full finite-sups-inheriting SubRelStr of S
for T9 being non empty full finite-sups-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is finite-sups-preserving
let f be finite-sups-preserving Function of S,T; :: thesis: for S9 being non empty full finite-sups-inheriting SubRelStr of S
for T9 being non empty full finite-sups-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is finite-sups-preserving
let S9 be non empty full finite-sups-inheriting SubRelStr of S; :: thesis: for T9 being non empty full finite-sups-inheriting SubRelStr of T
for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is finite-sups-preserving
let T9 be non empty full finite-sups-inheriting SubRelStr of T; :: thesis: for g being Function of S9,T9 st g = f | the carrier of S9 holds
g is finite-sups-preserving
let g be Function of S9,T9; :: thesis: ( g = f | the carrier of S9 implies g is finite-sups-preserving )
assume A1: g = f | the carrier of S9 ; :: thesis: g is finite-sups-preserving
Bottom S9 = Bottom S by Th60;
then g . (Bottom S9) = f . (Bottom S) by A1, FUNCT_1:49
.= Bottom T by Def17
.= Bottom T9 by Th60 ;
then g is bottom-preserving ;
hence g is finite-sups-preserving by A1, Th62, Th64; :: thesis: verum