let D, A, B be non empty set ; :: thesis: for H being Function of D,[:A,B:]
for d being Element of D holds H . d = [((pr1 H) . d),((pr2 H) . d)]
let H be Function of D,[:A,B:]; :: thesis: for d being Element of D holds H . d = [((pr1 H) . d),((pr2 H) . d)]
let d be Element of D; :: thesis: H . d = [((pr1 H) . d),((pr2 H) . d)]
thus H . d = [((H . d) `1),((H . d) `2)] by MCART_1:21
.= [((H . d) `1),((pr2 H) . d)] by Def6
.= [((pr1 H) . d),((pr2 H) . d)] by Def5 ; :: thesis: verum