let a be set ; :: thesis: for X, Y being set
for f being Function st a in dom f & f . a in [:X,Y:] holds
f . a = [((pr1 f) . a),((pr2 f) . a)]
let X, Y be set ; :: thesis: for f being Function st a in dom f & f . a in [:X,Y:] holds
f . a = [((pr1 f) . a),((pr2 f) . a)]
let f be Function; :: thesis: ( a in dom f & f . a in [:X,Y:] implies f . a = [((pr1 f) . a),((pr2 f) . a)] )
assume that
A1: a in dom f and
A2: f . a in [:X,Y:] ; :: thesis: f . a = [((pr1 f) . a),((pr2 f) . a)]
( (pr1 f) . a = (f . a) `1 & (pr2 f) . a = (f . a) `2 ) by A1, MCART_1:def 12, MCART_1:def 13;
hence f . a = [((pr1 f) . a),((pr2 f) . a)] by A2, MCART_1:21; :: thesis: verum