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:]
(Proj f,b) .: X = f .: [:{b},X:]
proof
thus
(Proj f,b) .: X c= f .: [:{b},X:]
:: according to XBOOLE_0:def 10 :: thesis: f .: [:{b},X:] c= (Proj f,b) .: Xproof
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 A1:
(
k in dom (Proj f,b) &
k in X &
c = (Proj f,b) . k )
by FUNCT_1:def 12;
A2:
c = f . b,
k
by A1, Th7;
b in {b}
by TARSKI:def 1;
then A3:
[b,k] in [:{b},X:]
by A1, 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
[b,k] in dom f
by A1, ZFMISC_1:106;
hence
c in f .: [:{b},X:]
by A2, A3, FUNCT_1:def 12;
:: thesis: verum
end;
thus
f .: [:{b},X:] c= (Proj f,b) .: X
:: thesis: verumproof
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 A4:
(
k in dom f &
k in [:{b},X:] &
c = f . k )
by FUNCT_1:def 12;
consider k1,
k2 being
set such that A5:
(
k1 in {b} &
k2 in X &
k = [k1,k2] )
by A4, ZFMISC_1:def 2;
A6:
dom (Proj f,b) = the
carrier of
S
by FUNCT_2:def 1;
A7:
c = f . k1,
k2
by A4, A5;
k1 = b
by A5, TARSKI:def 1;
then
c = (Proj f,b) . k2
by A5, A7, Th7;
hence
c in (Proj f,b) .: X
by A5, A6, FUNCT_1:def 12;
:: thesis: verum
end;
end;
hence
(Proj f,b) .: X = f .: [:{b},X:]
; :: thesis: verum