let n, i be Nat; for f being PartFunc of REAL,(REAL n)
for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A
let f be PartFunc of REAL,(REAL n); for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A
let A be Subset of REAL; (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A
A1:
dom (proj (i,n)) = REAL n
by FUNCT_2:def 1;
then A2:
rng f c= dom (proj (i,n))
;
A3:
rng (f | A) c= dom (proj (i,n))
by A1;
A4:
now for c being object st c in dom (((proj (i,n)) * f) | A) holds
(((proj (i,n)) * f) | A) . c = ((proj (i,n)) * (f | A)) . clet c be
object ;
( c in dom (((proj (i,n)) * f) | A) implies (((proj (i,n)) * f) | A) . c = ((proj (i,n)) * (f | A)) . c )assume A5:
c in dom (((proj (i,n)) * f) | A)
;
(((proj (i,n)) * f) | A) . c = ((proj (i,n)) * (f | A)) . cthen A6:
c in (dom ((proj (i,n)) * f)) /\ A
by RELAT_1:61;
A7:
c in dom ((proj (i,n)) * f)
by A6, XBOOLE_0:def 4;
then
c in dom f
by A2, RELAT_1:27;
then
c in (dom f) /\ A
by A5, XBOOLE_0:def 4;
then A8:
c in dom (f | A)
by RELAT_1:61;
then
c in dom ((proj (i,n)) * (f | A))
by A3, RELAT_1:27;
then ((proj (i,n)) * (f | A)) . c =
(proj (i,n)) . ((f | A) . c)
by FUNCT_1:12
.=
(proj (i,n)) . (f . c)
by A8, FUNCT_1:47
.=
((proj (i,n)) * f) . c
by A7, FUNCT_1:12
;
hence
(((proj (i,n)) * f) | A) . c = ((proj (i,n)) * (f | A)) . c
by A5, FUNCT_1:47;
verum end;
dom (((proj (i,n)) * f) | A) =
(dom ((proj (i,n)) * f)) /\ A
by RELAT_1:61
.=
(dom f) /\ A
by A2, RELAT_1:27
.=
dom (f | A)
by RELAT_1:61
.=
dom ((proj (i,n)) * (f | A))
by A3, RELAT_1:27
;
hence
(proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A
by A4, FUNCT_1:2; verum