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 ;
reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of ;
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) by XBOOLE_1:1;
A2: T |^ the carrier of S = product SYT by YELLOW_1:def 5;
reconsider X = F as Subset of (product SYT) by A1, YELLOW_1:def 5;
A3: 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 set ; :: 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 consider g being Function such that
A4: ( g in X & a = g . i ) by CARD_3:def 6;
thus a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } by A1, A4; :: 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 set ; :: 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 consider g being Element of (T |^ the carrier of S) such that
A5: ( a = g . i & g in F ) ;
thus a in pi X,i by A5, CARD_3:def 6; :: thesis: verum

end;

end;

for i being Element of S holds SYT . i is complete LATTICE by FUNCOP_1:13;
then ("\/" F,(T |^ the carrier of S)) . i = "\/" (pi X,i),(SYT . i) by A2, WAYBEL_3:32
.= "\/" { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T by A3, FUNCOP_1:13 ;
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