let X be non empty set ; for Y being Subset of X
for i being object holds (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y
let Y be Subset of X; for i being object holds (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y
let i be object ; (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y
per cases
( Y is empty or not Y is empty )
;
suppose A2:
not
Y is
empty
;
(proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y
for
x being
object holds
(
x in (proj (({i} --> X),i)) .: (product ({i} --> Y)) iff
x in Y )
proof
let x be
object ;
( x in (proj (({i} --> X),i)) .: (product ({i} --> Y)) iff x in Y )
assume
x in Y
;
x in (proj (({i} --> X),i)) .: (product ({i} --> Y))
then reconsider z =
x as
Element of
Y ;
ex
y being
object st
(
y in dom (proj (({i} --> X),i)) &
y in product ({i} --> Y) &
x = (proj (({i} --> X),i)) . y )
proof
set y =
{i} --> z;
take
{i} --> z
;
( {i} --> z in dom (proj (({i} --> X),i)) & {i} --> z in product ({i} --> Y) & x = (proj (({i} --> X),i)) . ({i} --> z) )
{i} --> z in product ({i} --> Y)
by A2, Th13;
then
{i} --> z in product ({i} --> X)
by Th14, TARSKI:def 3;
hence A7:
(
{i} --> z in dom (proj (({i} --> X),i)) &
{i} --> z in product ({i} --> Y) )
by A2, Th13, CARD_3:def 16;
x = (proj (({i} --> X),i)) . ({i} --> z)
thus x =
(i .--> z) . i
by FUNCOP_1:72
.=
({i} --> z) . i
by FUNCOP_1:def 9
.=
(proj (({i} --> X),i)) . ({i} --> z)
by A7, CARD_3:def 16
;
verum
end;
hence
x in (proj (({i} --> X),i)) .: (product ({i} --> Y))
by FUNCT_1:def 6;
verum
end; hence
(proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y
by TARSKI:2;
verum end; end;