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