let x, PI be Tuple of 4,X; :: thesis: ( x = <*(PI . 4),(PI . 2),(PI . 3),(PI . 1)*> implies PI = <*(x . 4),(x . 2),(x . 3),(x . 1)*> )
assume x = <*(PI . 4),(PI . 2),(PI . 3),(PI . 1)*> ; :: thesis: PI = <*(x . 4),(x . 2),(x . 3),(x . 1)*>
then ( x . 1 = PI . 4 & x . 2 = PI . 2 & x . 3 = PI . 3 & x . 4 = PI . 1 & len PI = 4 ) by CARD_1:def 7;
hence PI = <*(x . 4),(x . 2),(x . 3),(x . 1)*> by FINSEQ_4:76; :: thesis: verum