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
.= (i .--> z) . i by
.= 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 ;
then {i} --> z in product ({i} --> X) by ;
hence A7: ( {i} --> z in dom (proj (({i} --> X),i)) & {i} --> z in product ({i} --> Y) ) by ; :: 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 ; :: 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;