let R, S, T be LATTICE; :: thesis: for f being Function of [:R,S:],T
for b being Element of S
for X being Subset of R holds (Proj f,b) .: X = f .: [:X,{b}:]
let f be Function of [:R,S:],T; :: thesis: for b being Element of S
for X being Subset of R holds (Proj f,b) .: X = f .: [:X,{b}:]
let b be Element of S; :: thesis: for X being Subset of R holds (Proj f,b) .: X = f .: [:X,{b}:]
let X be Subset of R; :: thesis: (Proj f,b) .: X = f .: [:X,{b}:]
(Proj f,b) .: X = f .: [:X,{b}:]

proof

thus (Proj f,b) .: X c= f .: [:X,{b}:] :: according to XBOOLE_0:def 10 :: thesis: f .: [:X,{b}:] c= (Proj f,b) .: X

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in (Proj f,b) .: X or c in f .: [:X,{b}:] )
assume c in (Proj f,b) .: X ; :: thesis: c in f .: [:X,{b}:]
then consider k being set such that
A1: ( k in dom (Proj f,b) & k in X & c = (Proj f,b) . k ) by FUNCT_1:def 12;
A2: c = f . k,b by A1, Th8;
b in {b} by TARSKI:def 1;
then A3: [k,b] in [:X,{b}:] by A1, ZFMISC_1:106;
[:the carrier of R,the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def 2;
then dom f = [:the carrier of R,the carrier of S:] by FUNCT_2:def 1;
then [k,b] in dom f by A1, ZFMISC_1:106;
hence c in f .: [:X,{b}:] by A2, A3, FUNCT_1:def 12; :: thesis: verum

end;

thus f .: [:X,{b}:] c= (Proj f,b) .: X :: thesis: verum

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in f .: [:X,{b}:] or c in (Proj f,b) .: X )
assume c in f .: [:X,{b}:] ; :: thesis: c in (Proj f,b) .: X
then consider k being set such that
A4: ( k in dom f & k in [:X,{b}:] & c = f . k ) by FUNCT_1:def 12;
consider k1, k2 being set such that
A5: ( k1 in X & k2 in {b} & k = [k1,k2] ) by A4, ZFMISC_1:def 2;
A6: dom (Proj f,b) = the carrier of R by FUNCT_2:def 1;
A7: c = f . k1,k2 by A4, A5;
k2 = b by A5, TARSKI:def 1;
then c = (Proj f,b) . k1 by A5, A7, Th8;
hence c in (Proj f,b) .: X by A5, A6, FUNCT_1:def 12; :: thesis: verum

end;

end;

hence (Proj f,b) .: X = f .: [:X,{b}:] ; :: thesis: verum