let x1, x2, x3, x4 be set ; :: thesis: for p being FinSequence holds
( p = <*x1,x2,x3,x4*> iff ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) )
let p be FinSequence; :: thesis: ( p = <*x1,x2,x3,x4*> iff ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) )
thus ( p = <*x1,x2,x3,x4*> implies ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) ) :: thesis: ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 implies p = <*x1,x2,x3,x4*> )

proof

assume A1: p = <*x1,x2,x3,x4*> ; :: thesis: ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
hence len p = (len <*x1,x2,x3*>) + (len <*x4*>) by FINSEQ_1:35
.= 3 + (len <*x4*>) by FINSEQ_1:62
.= 3 + 1 by FINSEQ_1:57
.= 4 ;
:: thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
set p3 = <*x1,x2,x3*>;
A2: dom <*x1,x2,x3*> = {1,2,3} by FINSEQ_3:1, FINSEQ_3:30;
then 1 in dom <*x1,x2,x3*> by ENUMSET1:def 1;
hence p . 1 = <*x1,x2,x3*> . 1 by A1, FINSEQ_1:def 7
.= x1 by FINSEQ_1:62 ;
:: thesis: ( p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
2 in dom <*x1,x2,x3*> by A2, ENUMSET1:def 1;
hence p . 2 = <*x1,x2,x3*> . 2 by A1, FINSEQ_1:def 7
.= x2 by FINSEQ_1:62 ;
:: thesis: ( p . 3 = x3 & p . 4 = x4 )
3 in dom <*x1,x2,x3*> by A2, ENUMSET1:def 1;
hence p . 3 = <*x1,x2,x3*> . 3 by A1, FINSEQ_1:def 7
.= x3 by FINSEQ_1:62 ;
:: thesis: p . 4 = x4
1 in {1} by TARSKI:def 1;
then A3: 1 in dom <*x4*> by FINSEQ_1:4, FINSEQ_1:def 8;
thus p . 4 = (<*x1,x2,x3*> ^ <*x4*>) . (3 + 1) by A1
.= (<*x1,x2,x3*> ^ <*x4*>) . ((len <*x1,x2,x3*>) + 1) by FINSEQ_1:62
.= <*x4*> . 1 by A3, FINSEQ_1:def 7
.= x4 by FINSEQ_1:def 8 ; :: thesis: verum

end;

assume A4: ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) ; :: thesis: p = <*x1,x2,x3,x4*>
then A5: dom p = Seg (3 + 1) by FINSEQ_1:def 3
.= Seg ((len <*x1,x2,x3*>) + 1) by FINSEQ_1:62
.= Seg ((len <*x1,x2,x3*>) + (len <*x4*>)) by FINSEQ_1:56 ;
A6: for k being Nat st k in dom <*x1,x2,x3*> holds
p . k = <*x1,x2,x3*> . k

proof

let k be Nat; :: thesis: ( k in dom <*x1,x2,x3*> implies p . k = <*x1,x2,x3*> . k )
assume A7: k in dom <*x1,x2,x3*> ; :: thesis: p . k = <*x1,x2,x3*> . k
len <*x1,x2,x3*> = 3 by FINSEQ_1:62;
then A8: k in {1,2,3} by A7, FINSEQ_1:def 3, FINSEQ_3:1;

per cases ( k = 1 or k = 2 or k = 3 ) by A8, ENUMSET1:def 1;

suppose k = 1 ; :: thesis: p . k = <*x1,x2,x3*> . k

hence p . k = <*x1,x2,x3*> . k by A4, FINSEQ_1:62; :: thesis: verum

end;

suppose k = 2 ; :: thesis: p . k = <*x1,x2,x3*> . k

hence p . k = <*x1,x2,x3*> . k by A4, FINSEQ_1:62; :: thesis: verum

end;

suppose k = 3 ; :: thesis: p . k = <*x1,x2,x3*> . k

hence p . k = <*x1,x2,x3*> . k by A4, FINSEQ_1:62; :: thesis: verum

end;

end;

end;

for k being Nat st k in dom <*x4*> holds
p . ((len <*x1,x2,x3*>) + k) = <*x4*> . k

proof

let k be Nat; :: thesis: ( k in dom <*x4*> implies p . ((len <*x1,x2,x3*>) + k) = <*x4*> . k )
assume k in dom <*x4*> ; :: thesis: p . ((len <*x1,x2,x3*>) + k) = <*x4*> . k
then k in {1} by FINSEQ_1:4, FINSEQ_1:def 8;
then A9: k = 1 by TARSKI:def 1;
hence p . ((len <*x1,x2,x3*>) + k) = p . (3 + 1) by FINSEQ_1:62
.= <*x4*> . k by A4, A9, FINSEQ_1:def 8 ;
:: thesis: verum

end;

hence p = <*x1,x2,x3,x4*> by A5, A6, FINSEQ_1:def 7; :: thesis: verum