let R, S, T be LATTICE; 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; 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; for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]
let X be Subset of S; (Proj (f,b)) .: X = f .: [:{b},X:]
A1:
(Proj (f,b)) .: X c= f .: [:{b},X:]
proof
let c be
object ;
TARSKI:def 3 ( not c in (Proj (f,b)) .: X or c in f .: [:{b},X:] )
assume
c in (Proj (f,b)) .: X
;
c in f .: [:{b},X:]
then consider k being
object 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;
verum
end;
f .: [:{b},X:] c= (Proj (f,b)) .: X
proof
let c be
object ;
TARSKI:def 3 ( not c in f .: [:{b},X:] or c in (Proj (f,b)) .: X )
assume
c in f .: [:{b},X:]
;
c in (Proj (f,b)) .: X
then consider k being
object 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
object 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;
verum
end;
hence
(Proj (f,b)) .: X = f .: [:{b},X:]
by A1; verum