let S, T be complete TopLattice; :: thesis: for F being non empty Subset of (ContMaps (S,T))
for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)
let F be non empty Subset of (ContMaps (S,T)); :: thesis: for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)
let i be Element of S; :: thesis: ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)
reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ;
reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ;
ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3;
then the carrier of (ContMaps (S,T)) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def 13;
then A1: F c= the carrier of (T |^ the carrier of S) ;
then reconsider X = F as Subset of (product SYT) by YELLOW_1:def 5;
A2: pi (X,i) = { (f . i) where f is Element of (T |^ the carrier of S) : f in F }

proof

thus pi (X,i) c= { (f . i) where f is Element of (T |^ the carrier of S) : f in F } :: according to XBOOLE_0:def 10 :: thesis: { (f . i) where f is Element of (T |^ the carrier of S) : f in F } c= pi (X,i)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in pi (X,i) or a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } )
assume a in pi (X,i) ; :: thesis: a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F }
then ex g being Function st
( g in X & a = g . i ) by CARD_3:def 6;
hence a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } by A1; :: thesis: verum

end;

thus { (f . i) where f is Element of (T |^ the carrier of S) : f in F } c= pi (X,i) :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } or a in pi (X,i) )
assume a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ; :: thesis: a in pi (X,i)
then ex g being Element of (T |^ the carrier of S) st
( a = g . i & g in F ) ;
hence a in pi (X,i) by CARD_3:def 6; :: thesis: verum

end;

end;

( T |^ the carrier of S = product SYT & ( for i being Element of S holds SYT . i is complete LATTICE ) ) by FUNCOP_1:7, YELLOW_1:def 5;
then ("\/" (F,(T |^ the carrier of S))) . i = "\/" ((pi (X,i)),(SYT . i)) by WAYBEL_3:32
.= "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) by A2, FUNCOP_1:7 ;
hence ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) ; :: thesis: verum