theorem Th57: :: MATRIX11:57

for X being set
for Y being non empty set
for x being object st not x in X holds
ex BIJECT being Function of [:(Funcs (X,Y)),Y:],(Funcs ((X \/ {x}),Y)) st
( BIJECT is bijective & ( for f being Function of X,Y
for F being Function of (X \/ {x}),Y st F | X = f holds
BIJECT . (f,(F . x)) = F ) )