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 = sup {(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 = sup {(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 = sup {(f . i),(g . i)}
let i be Element of S; :: thesis: ( h = "\/" {f,g},(T |^ the carrier of S) implies h . i = sup {(f . i),(g . i)} )
assume A1: h = "\/" {f,g},(T |^ the carrier of S) ; :: thesis: h . i = sup {(f . i),(g . i)}
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 ;
A2: for i being Element of S holds SYT . i is complete LATTICE by FUNCOP_1:13;
reconsider f' = f, g' = g as Element of (T |^ the carrier of S) by Th19;
reconsider f' = f', g' = g' as Element of (product SYT) by YELLOW_1:def 5;
reconsider DU = {f',g'} as Subset of (product SYT) ;
h . i = (sup DU) . i by A1, YELLOW_1:def 5
.= "\/" (pi {f,g},i),(SYT . i) by A2, WAYBEL_3:32
.= "\/" (pi {f,g},i),T by FUNCOP_1:13
.= sup {(f . i),(g . i)} by CARD_3:26 ;
hence h . i = sup {(f . i),(g . i)} ; :: thesis: verum