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