let x1, x2, x3, x4 be object ; :: 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

set p3 = <*x1,x2,x3*>;
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:22
.= 3 + (len <*x4*>) by FINSEQ_1:45
.= 3 + 1 by FINSEQ_1:40
.= 4 ;
:: thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
A2: dom <*x1,x2,x3*> = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;
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 ;
:: 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 ;
:: 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 ;
:: thesis: p . 4 = x4
1 in {1} by TARSKI:def 1;
then A3: 1 in dom <*x4*> by FINSEQ_1:2, 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:45
.= <*x4*> . 1 by A3, FINSEQ_1:def 7
.= x4 ; :: thesis: verum

end;

assume that
A4: len p = 4 and
A5: p . 1 = x1 and
A6: p . 2 = x2 and
A7: p . 3 = x3 and
A8: p . 4 = x4 ; :: thesis: p = <*x1,x2,x3,x4*>
A9: for k being Nat st k in dom <*x1,x2,x3*> holds
p . k = <*x1,x2,x3*> . k

proof

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

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

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

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

end;

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

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

end;

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

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

end;

end;

end;

A12: 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:2, FINSEQ_1:def 8;
then A13: k = 1 by TARSKI:def 1;
hence p . ((len <*x1,x2,x3*>) + k) = p . (3 + 1) by FINSEQ_1:45
.= <*x4*> . k by A8, A13 ;
:: thesis: verum

end;

dom p = Seg (3 + 1) by A4, FINSEQ_1:def 3
.= Seg ((len <*x1,x2,x3*>) + 1) by FINSEQ_1:45
.= Seg ((len <*x1,x2,x3*>) + (len <*x4*>)) by FINSEQ_1:39 ;
hence p = <*x1,x2,x3,x4*> by A9, A12, FINSEQ_1:def 7; :: thesis: verum