let R, S, T be LATTICE; :: thesis: for f being Function of [:R,S:],T
for b being Element of R
for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]
let f be Function of [:R,S:],T; :: thesis: for b being Element of R
for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]
let b be Element of R; :: thesis: for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]
let X be Subset of S; :: thesis: (Proj (f,b)) .: X = f .: [:{b},X:]
A1: (Proj (f,b)) .: X c= 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 .: [:{b},X:] )
assume c in (Proj (f,b)) .: X ; :: thesis: c in f .: [:{b},X:]
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: [b,k] in [:{b},X:] 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: [b,k] in dom f by A2, ZFMISC_1:87;
c = f . (b,k) by A2, A4, Th7;
hence c in f .: [:{b},X:] by A5, A6, FUNCT_1:def 6; :: thesis: verum

end;

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

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in f .: [:{b},X:] or c in (Proj (f,b)) .: X )
assume c in f .: [:{b},X:] ; :: thesis: c in (Proj (f,b)) .: X
then consider k being set such that
k in dom f and
A7: k in [:{b},X:] and
A8: c = f . k by FUNCT_1:def 6;
consider k1, k2 being set such that
A9: k1 in {b} and
A10: k2 in X and
A11: k = [k1,k2] by A7, ZFMISC_1:def 2;
A12: k1 = b by A9, TARSKI:def 1;
c = f . (k1,k2) by A8, A11;
then ( dom (Proj (f,b)) = the carrier of S & c = (Proj (f,b)) . k2 ) by A10, A12, Th7, FUNCT_2:def 1;
hence c in (Proj (f,b)) .: X by A10, FUNCT_1:def 6; :: thesis: verum

end;

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