let X be non empty set ; :: thesis: 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; :: thesis: for i being object holds (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y

let i be object ; :: thesis: (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y

for i being object holds (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y

let Y be Subset of X; :: thesis: for i being object holds (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y

let i be object ; :: thesis: (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y

per cases
( Y is empty or not Y is empty )
;

end;

suppose A1:
Y is empty
; :: thesis: (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y

then
rng ({i} --> Y) = {{}}
by FUNCOP_1:8;

then product ({i} --> Y) = {} by Lm1;

hence (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y by A1; :: thesis: verum

end;then product ({i} --> Y) = {} by Lm1;

hence (proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y by A1; :: thesis: verum

suppose A2:
not Y is empty
; :: thesis: (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 )

end;( x in (proj (({i} --> X),i)) .: (product ({i} --> Y)) iff x in Y )

proof

hence
(proj (({i} --> X),i)) .: (product ({i} --> Y)) = Y
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in (proj (({i} --> X),i)) .: (product ({i} --> Y)) iff x in 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 )

end;hereby :: thesis: ( x in Y implies x in (proj (({i} --> X),i)) .: (product ({i} --> Y)) )

assume
x in Y
; :: thesis: x in (proj (({i} --> X),i)) .: (product ({i} --> Y))assume
x in (proj (({i} --> X),i)) .: (product ({i} --> Y))
; :: thesis: x in Y

then consider y being object such that

A3: ( y in dom (proj (({i} --> X),i)) & y in product ({i} --> Y) ) and

A4: x = (proj (({i} --> X),i)) . y by FUNCT_1:def 6;

consider z being Element of Y such that

A5: y = {i} --> z by A2, A3, Th16;

reconsider y = y as Function by A5;

x = y . i by A3, A4, CARD_3:def 16

.= (i .--> z) . i by A5, FUNCOP_1:def 9

.= z by FUNCOP_1:72 ;

hence x in Y by A2; :: thesis: verum

end;then consider y being object such that

A3: ( y in dom (proj (({i} --> X),i)) & y in product ({i} --> Y) ) and

A4: x = (proj (({i} --> X),i)) . y by FUNCT_1:def 6;

consider z being Element of Y such that

A5: y = {i} --> z by A2, A3, Th16;

reconsider y = y as Function by A5;

x = y . i by A3, A4, CARD_3:def 16

.= (i .--> z) . i by A5, FUNCOP_1:def 9

.= z by FUNCOP_1:72 ;

hence x in Y by A2; :: thesis: verum

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

hence
x in (proj (({i} --> X),i)) .: (product ({i} --> Y))
by FUNCT_1:def 6; :: thesis: verum
set y = {i} --> z;

take {i} --> z ; :: thesis: ( {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; :: thesis: 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 ; :: thesis: verum

end;take {i} --> z ; :: thesis: ( {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; :: thesis: 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 ; :: thesis: verum