let S be non empty 1-sorted ; :: thesis: for T being complete LATTICE
for f, g, h being Function of S,T
for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds
h . i = inf {(f . i),(g . i)}
let T be complete LATTICE; :: thesis: for f, g, h being Function of S,T
for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds
h . i = inf {(f . i),(g . i)}
let f, g, h be Function of S,T; :: thesis: for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds
h . i = inf {(f . i),(g . i)}
let i be Element of S; :: thesis: ( h = "/\" ({f,g},(T |^ the carrier of S)) implies h . i = inf {(f . i),(g . i)} )
reconsider f9 = f, g9 = g as Element of (T |^ the carrier of S) by Th19;
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 ;
A1: for i being Element of S holds SYT . i is complete LATTICE by FUNCOP_1:7;
reconsider f9 = f9, g9 = g9 as Element of (product SYT) by YELLOW_1:def 5;
reconsider DU = {f9,g9} as Subset of (product SYT) ;
assume h = "/\" ({f,g},(T |^ the carrier of S)) ; :: thesis: h . i = inf {(f . i),(g . i)}
then h . i = (inf DU) . i by YELLOW_1:def 5
.= "/\" ((pi ({f,g},i)),(SYT . i)) by A1, Th23
.= "/\" ((pi ({f,g},i)),T) by FUNCOP_1:7
.= inf {(f . i),(g . i)} by CARD_3:15 ;
hence h . i = inf {(f . i),(g . i)} ; :: thesis: verum