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

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

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;

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 )

proof

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

hereby :: thesis: ( x in Y implies 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;

assume x in Y ; :: thesis: 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 ; :: 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;

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

end;

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

end;

end;