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
g is bottom-preserving

proof

( Bottom S' = Bottom S & the carrier of T <> {} ) by Th64;
hence g . (Bottom S') = f . (Bottom S) by A1, FUNCT_1:72
.= Bottom T by Def17
.= Bottom T' by Th64 ;
:: according to WAYBEL34:def 17 :: thesis: verum

end;

hence g is finite-sups-preserving by A1, Th66, Th68; :: thesis: verum