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

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