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