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}:]
A1: (Proj f,b) .: X c= f .: [:X,{b}:]

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
A2: k in dom (Proj f,b) and
A3: k in X and
A4: c = (Proj f,b) . k by FUNCT_1:def 12;
b in {b} by TARSKI:def 1;
then A5: [k,b] in [:X,{b}:] by A3, 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 A6: [k,b] in dom f by A2, ZFMISC_1:106;
c = f . k,b by A2, A4, Th8;
hence c in f .: [:X,{b}:] by A5, A6, FUNCT_1:def 12; :: thesis: verum

end;

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

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
k in dom f and
A7: k in [:X,{b}:] and
A8: c = f . k by FUNCT_1:def 12;
consider k1, k2 being set such that
A9: k1 in X and
A10: k2 in {b} and
A11: k = [k1,k2] by A7, ZFMISC_1:def 2;
A12: k2 = b by A10, TARSKI:def 1;
c = f . k1,k2 by A8, A11;
then ( dom (Proj f,b) = the carrier of R & c = (Proj f,b) . k1 ) by A9, A12, Th8, FUNCT_2:def 1;
hence c in (Proj f,b) .: X by A9, FUNCT_1:def 12; :: thesis: verum

end;

hence (Proj f,b) .: X = f .: [:X,{b}:] by A1, XBOOLE_0:def 10; :: thesis: verum