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