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