let r, p be Element of Prop Q; :: thesis: ( r = [(p `1),((p `2) `)] implies p = [(r `1),((r `2) `)] )
assume A1: r = [(p `1),((p `2) `)] ; :: thesis: p = [(r `1),((r `2) `)]
thus p = [(p `1),(((p `2) `) `)] by MCART_1:21
.= [(r `1),(((p `2) `) `)] by A1, MCART_1:7
.= [(r `1),((r `2) `)] by A1, MCART_1:7 ; :: thesis: verum