let F be Function; for i being set st i in dom F holds
( rng (proj (F,i)) c= F . i & ( product F <> {} implies rng (proj (F,i)) = F . i ) )
let i be set ; ( i in dom F implies ( rng (proj (F,i)) c= F . i & ( product F <> {} implies rng (proj (F,i)) = F . i ) ) )
assume A1:
i in dom F
; ( rng (proj (F,i)) c= F . i & ( product F <> {} implies rng (proj (F,i)) = F . i ) )
thus A2:
rng (proj (F,i)) c= F . i
( product F <> {} implies rng (proj (F,i)) = F . i )proof
let x be
object ;
TARSKI:def 3 ( not x in rng (proj (F,i)) or x in F . i )
assume
x in rng (proj (F,i))
;
x in F . i
then consider f9 being
object such that A3:
f9 in dom (proj (F,i))
and A4:
x = (proj (F,i)) . f9
by FUNCT_1:def 3;
f9 in product F
by A3;
then consider f being
Function such that A5:
f9 = f
and
dom f = dom F
and A6:
for
x being
object st
x in dom F holds
f . x in F . x
by CARD_3:def 5;
(proj (F,i)) . f = f . i
by A3, A5, CARD_3:def 16;
hence
x in F . i
by A1, A4, A5, A6;
verum
end;
assume A7:
product F <> {}
; rng (proj (F,i)) = F . i
thus
rng (proj (F,i)) c= F . i
by A2; XBOOLE_0:def 10 F . i c= rng (proj (F,i))
let x be object ; TARSKI:def 3 ( not x in F . i or x in rng (proj (F,i)) )
set f9 = the Element of product F;
consider f being Function such that
A8:
the Element of product F = f
and
A9:
dom f = dom F
and
for x being object st x in dom F holds
f . x in F . x
by A7, CARD_3:def 5;
assume
x in F . i
; x in rng (proj (F,i))
then
f +* (i,x) in product F
by A7, A8, Th2;
then A10:
f +* (i,x) in dom (proj (F,i))
by CARD_3:def 16;
(f +* (i,x)) . i = x
by A1, A9, FUNCT_7:31;
then
(proj (F,i)) . (f +* (i,x)) = x
by A10, CARD_3:def 16;
hence
x in rng (proj (F,i))
by A10, FUNCT_1:def 3; verum