let X be set ; :: thesis: for L being non empty complete continuous Poset
for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f
let L be non empty complete continuous Poset; :: thesis: for f being Function of (FixedUltraFilters X), the carrier of L holds (f -extension_to_hom) | (FixedUltraFilters X) = f
let f be Function of (FixedUltraFilters X), the carrier of L; :: thesis: (f -extension_to_hom) | (FixedUltraFilters X) = f
set FUF = FixedUltraFilters X;
set BP = BoolePoset X;
set IP = InclPoset (Filt (BoolePoset X));
A1: InclPoset (Filt (BoolePoset X)) = RelStr(# (Filt (BoolePoset X)),(RelIncl (Filt (BoolePoset X))) #) by YELLOW_1:def 1;
set F = f -extension_to_hom ;
A2: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def 2
.= bool X by LATTICE3:def 1 ;

now :: thesis: ( FixedUltraFilters X = dom ((f -extension_to_hom) | (FixedUltraFilters X)) & FixedUltraFilters X = dom f & ( for xf being object st xf in FixedUltraFilters X holds
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf ) )

A3: dom (f -extension_to_hom) = the carrier of (InclPoset (Filt (BoolePoset X))) by FUNCT_2:def 1;
hence FixedUltraFilters X = dom ((f -extension_to_hom) | (FixedUltraFilters X)) by A1, Th9, RELAT_1:62; :: thesis: ( FixedUltraFilters X = dom f & ( for xf being object st xf in FixedUltraFilters X holds
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf ) )
thus FixedUltraFilters X = dom f by FUNCT_2:def 1; :: thesis: for xf being object st xf in FixedUltraFilters X holds
((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf
let xf be object ; :: thesis: ( xf in FixedUltraFilters X implies ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf )
assume A4: xf in FixedUltraFilters X ; :: thesis: ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf
then reconsider FUF9 = FixedUltraFilters X as non empty Subset-Family of (BoolePoset X) ;
A5: ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = (f -extension_to_hom) . xf by A4, FUNCT_1:49;
FixedUltraFilters X c= dom (f -extension_to_hom) by A1, A3, Th9;
then reconsider x9 = xf as Element of (InclPoset (Filt (BoolePoset X))) by A4, FUNCT_2:def 1;
reconsider xf9 = xf as Element of FUF9 by A4;
set Xs = { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } ;
reconsider f9 = f as Function of FUF9, the carrier of L ;
f9 . xf9 is Element of L ;
then reconsider fxf = f . xf9 as Element of L ;
consider xx being Element of (BoolePoset X) such that
A6: xf = uparrow xx and
A7: ex y being Element of X st xx = {y} by A4;
A8: { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } is_<=_than fxf

proof

let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } or b <= fxf )
assume b in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } ; :: thesis: b <= fxf
then consider Y being Subset of X such that
A9: b = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) and
A10: Y in x9 ;
set Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
ex_inf_of { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L by YELLOW_0:17;
then A11: { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } is_>=_than b by A9, YELLOW_0:def 10;
reconsider Y = Y as Element of (BoolePoset X) by A6, A10;
consider y being Element of X such that
A12: xx = {y} by A7;
xx <= Y by A6, A10, WAYBEL_0:18;
then xx c= Y by YELLOW_1:2;
then y in Y by A12, ZFMISC_1:31;
then fxf in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by A6, A12;
hence b <= fxf by A11; :: thesis: verum

end;

A13: for a being Element of L st { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } is_<=_than a holds
fxf <= a

proof

xx <= xx ;
then reconsider Y = xx as Element of x9 by A6, WAYBEL_0:18;
set Xsi = { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ;
consider y being Element of X such that
A14: xx = {y} by A7;

now :: thesis: for p being object holds
( ( p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } implies p in {fxf} ) & ( p in {fxf} implies p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ) )

let p be object ; :: thesis: ( ( p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } implies p in {fxf} ) & ( p in {fxf} implies p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ) )

hereby :: thesis: ( p in {fxf} implies p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } )

assume p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ; :: thesis: p in {fxf}
then consider r being Element of (BoolePoset X) such that
A15: p = f . (uparrow r) and
A16: ex z being Element of X st
( r = {z} & z in Y ) ;
xx = r by A14, A16, TARSKI:def 1;
hence p in {fxf} by A6, A15, TARSKI:def 1; :: thesis: verum

end;

assume p in {fxf} ; :: thesis: p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) }
then A17: p = fxf by TARSKI:def 1;
y in Y by A14, TARSKI:def 1;
hence p in { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } by A6, A14, A17; :: thesis: verum

end;

then { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } = {fxf} by TARSKI:2;
then fxf = "/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L) by YELLOW_0:39;
then A18: fxf in { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } by A2;
let a be Element of L; :: thesis: ( { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } is_<=_than a implies fxf <= a )
assume { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } is_<=_than a ; :: thesis: fxf <= a
hence fxf <= a by A18; :: thesis: verum

end;

ex_sup_of { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } ,L by YELLOW_0:17;
then f . xf = "\/" ( { ("/\" ( { (f . (uparrow x)) where x is Element of (BoolePoset X) : ex z being Element of X st
( x = {z} & z in Y ) } ,L)) where Y is Subset of X : Y in x9 } ,L) by A8, A13, YELLOW_0:def 9;
hence ((f -extension_to_hom) | (FixedUltraFilters X)) . xf = f . xf by A5, Def3; :: thesis: verum

end;

hence (f -extension_to_hom) | (FixedUltraFilters X) = f ; :: thesis: verum