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

end;

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