let X be non empty set ; :: thesis: for i being object
for x being Element of X holds (proj (({i} --> X),i)) . ({i} --> x) = x
let i be object ; :: thesis: for x being Element of X holds (proj (({i} --> X),i)) . ({i} --> x) = x
let x be Element of X; :: thesis: (proj (({i} --> X),i)) . ({i} --> x) = x
{i} --> x in product ({i} --> X) by Th13;
then {i} --> x in dom (proj (({i} --> X),i)) by CARD_3:def 16;
hence (proj (({i} --> X),i)) . ({i} --> x) = ({i} --> x) . i by CARD_3:def 16
.= (i .--> x) . i by FUNCOP_1:def 9
.= x by FUNCOP_1:72 ;
:: thesis: verum