set IT = Y |^ X;
let x, y be Element of (Y |^ X); :: according to LATTICE3:def 11 :: thesis: ex b1 being Element of the carrier of (Y |^ X) st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of (Y |^ X) holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
reconsider y9 = y as Function of X, the carrier of Y by Lm5;
reconsider x9 = x as Function of X, the carrier of Y by Lm5;
defpred S1[ object , object ] means ex xa, ya being Element of Y st
( xa = x9 . X & ya = y9 . X & Y = xa "/\" ya );
A1: for x being object st x in X holds
ex y being object st
( y in the carrier of Y & S1[x,y] )
proof
let a be object ; :: thesis: ( a in X implies ex y being object st
( y in the carrier of Y & S1[a,y] ) )
assume a in X ; :: thesis: ex y being object st
( y in the carrier of Y & S1[a,y] )
then reconsider xa = x9 . a, ya = y9 . a as Element of Y by FUNCT_2:5;
take y = xa "/\" ya; :: thesis: ( y in the carrier of Y & S1[a,y] )
thus y in the carrier of Y ; :: thesis: S1[a,y]
take xa ; :: thesis: ex ya being Element of Y st
( xa = x9 . a & ya = y9 . a & y = xa "/\" ya )
take ya ; :: thesis: ( xa = x9 . a & ya = y9 . a & y = xa "/\" ya )
thus ( xa = x9 . a & ya = y9 . a & y = xa "/\" ya ) ; :: thesis: verum
end;
consider f being Function of X, the carrier of Y such that
A2: for a being object st a in X holds
S1[a,f . a] from FUNCT_2:sch 1(A1);
 f in Funcs (X, the carrier of Y) by FUNCT_2:8;
then reconsider z = f as Element of (Y |^ X) by Th28;
take z ; :: thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of (Y |^ X) holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )
A3: z <= y
proof
reconsider y1 = y, z1 = z as Element of (product (X --> Y)) ;
A4: ex f, g being Function st
( f = z1 & g = y1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take f ; :: thesis: ex g being Function st
( f = z1 & g = y1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
take y9 ; :: thesis: ( f = z1 & y9 = y1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi ) ) )
thus ( f = z1 & y9 = y1 ) ; :: thesis: for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
let i be object ; :: thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi ) )
assume i in X ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider xi = f . i, yi = y9 . i as Element of R ;
take R ; :: thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
take xi ; :: thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi )
( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "/\" ya ) ) by A2;
hence ( R = (X --> Y) . i & xi = f . i & yi = y9 . i & xi <= yi ) by YELLOW_0:23; :: thesis: verum
end;
z1 in the carrier of (product (X --> Y)) ;
then z1 in product (Carrier (X --> Y)) by Def4;
hence z <= y by A4, Def4; :: thesis: verum
end;
A5: for z9 being Element of (Y |^ X) st z9 <= x & z9 <= y holds
z9 <= z
proof
let z9 be Element of (Y |^ X); :: thesis: ( z9 <= x & z9 <= y implies z9 <= z )
assume that
A6: z9 <= x and
A7: z9 <= y ; :: thesis: z9 <= z
z9 <= z
proof
reconsider z2 = z9, z3 = z, z4 = y, z5 = x as Element of (product (X --> Y)) ;
reconsider J = z2, K = z3 as Function of X, the carrier of Y by Lm5;
z9 in the carrier of (product (X --> Y)) ;
then A8: z2 in product (Carrier (X --> Y)) by Def4;
then consider f1, g1 being Function such that
A9: ( f1 = z2 & g1 = z5 ) and
A10: for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f1 . i & yi = g1 . i & xi <= yi ) by A6, Def4;
consider f2, g2 being Function such that
A11: ( f2 = z2 & g2 = z4 ) and
A12: for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f2 . i & yi = g2 . i & xi <= yi ) by A7, A8, Def4;
ex f, g being Function st
( f = z2 & g = z3 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take J ; :: thesis: ex g being Function st
( J = z2 & g = z3 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = g . i & xi <= yi ) ) )
take K ; :: thesis: ( J = z2 & K = z3 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi ) ) )
thus ( J = z2 & K = z3 ) ; :: thesis: for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
let i be object ; :: thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi ) )
assume i in X ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider xi = J . i, yi = K . i as Element of R ;
take R ; :: thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
take xi ; :: thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi )
A13: ( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "/\" ya ) ) by A2;
( ex R1 being RelStr ex xi1, yi1 being Element of R1 st
( R1 = (X --> Y) . i & xi1 = f1 . i & yi1 = g1 . i & xi1 <= yi1 ) & ex R2 being RelStr ex xi2, yi2 being Element of R2 st
( R2 = (X --> Y) . i & xi2 = f2 . i & yi2 = g2 . i & xi2 <= yi2 ) ) by A10, A12;
hence ( R = (X --> Y) . i & xi = J . i & yi = K . i & xi <= yi ) by A9, A11, A13, YELLOW_0:23; :: thesis: verum
end;
hence z9 <= z by A8, Def4; :: thesis: verum
end;
hence z9 <= z ; :: thesis: verum
end;
z <= x
proof
reconsider x1 = x, z1 = z as Element of (product (X --> Y)) ;
A14: ex f, g being Function st
( f = z1 & g = x1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
proof
take f ; :: thesis: ex g being Function st
( f = z1 & g = x1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
take x9 ; :: thesis: ( f = z1 & x9 = x1 & ( for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi ) ) )
thus ( f = z1 & x9 = x1 ) ; :: thesis: for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
let i be object ; :: thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi ) )
assume i in X ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
then reconsider i = i as Element of X ;
reconsider R = (X --> Y) . i as RelStr ;
reconsider xi = f . i, yi = x9 . i as Element of R ;
take R ; :: thesis: ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
take xi ; :: thesis: ex yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
take yi ; :: thesis: ( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi )
( R = Y & ex xa, ya being Element of Y st
( xa = x9 . i & ya = y9 . i & f . i = xa "/\" ya ) ) by A2;
hence ( R = (X --> Y) . i & xi = f . i & yi = x9 . i & xi <= yi ) by YELLOW_0:23; :: thesis: verum
end;
z1 in the carrier of (product (X --> Y)) ;
then z1 in product (Carrier (X --> Y)) by Def4;
hence z <= x by A14, Def4; :: thesis: verum
end;
hence ( z <= x & z <= y & ( for b1 being Element of the carrier of (Y |^ X) holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) ) by A3, A5; :: thesis: verum