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