set IP = InclPoset (Filt (BoolePoset X));
let it1, it2 be Function of (InclPoset (Filt (BoolePoset X))),L; :: thesis: ( ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it1 . Fi = "\/" { ("/\" { (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 Fi } ,L ) & ( for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it2 . Fi = "\/" { ("/\" { (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 Fi } ,L ) implies it1 = it2 )
assume that
A2: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it1 . Fi = "\/" { ("/\" { (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 Fi } ,L and
A3: for Fi being Element of (InclPoset (Filt (BoolePoset X))) holds it2 . Fi = "\/" { ("/\" { (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 Fi } ,L ; :: thesis: it1 = it2
reconsider it1' = it1 as Function of the carrier of (InclPoset (Filt (BoolePoset X))),the carrier of L ;
reconsider it2' = it2 as Function of the carrier of (InclPoset (Filt (BoolePoset X))),the carrier of L ;

now

let Fi be Element of (InclPoset (Filt (BoolePoset X))); :: thesis: it1' . Fi = it2' . Fi
thus it1' . Fi = "\/" { ("/\" { (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 Fi } ,L by A2
.= it2' . Fi by A3 ; :: thesis: verum

end;

hence it1 = it2 by FUNCT_2:113; :: thesis: verum