let x1, x2, x3, x4, x5 be object ; :: thesis: for p being FinSequence holds
( p = <*x1,x2,x3,x4,x5*> iff ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) )
let p be FinSequence; :: thesis: ( p = <*x1,x2,x3,x4,x5*> iff ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) )
set p4 = <*x1,x2,x3,x4*>;
thus ( p = <*x1,x2,x3,x4,x5*> implies ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) ) :: thesis: ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 implies p = <*x1,x2,x3,x4,x5*> )
proof
set p4 = <*x1,x2,x3,x4*>;
1 in {1} by TARSKI:def 1;
then A1: 1 in dom <*x5*> by FINSEQ_1:2, FINSEQ_1:def 8;
assume A2: p = <*x1,x2,x3,x4,x5*> ; :: thesis: ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
then A3: p = <*x1,x2,x3,x4*> ^ <*x5*> by Th75;
thus len p = len (<*x1,x2,x3,x4*> ^ <*x5*>) by A2, Th75
.= (len <*x1,x2,x3,x4*>) + (len <*x5*>) by FINSEQ_1:22
.= 4 + (len <*x5*>) by Th76
.= 4 + 1 by FINSEQ_1:40
.= 5 ; :: thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
A4: dom <*x1,x2,x3,x4*> = {1,2,3,4} by FINSEQ_1:89, FINSEQ_3:2;
then 1 in dom <*x1,x2,x3,x4*> by ENUMSET1:def 2;
hence p . 1 = <*x1,x2,x3,x4*> . 1 by A3, FINSEQ_1:def 7
.= x1 by Th76 ;
:: thesis: ( p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
2 in dom <*x1,x2,x3,x4*> by A4, ENUMSET1:def 2;
hence p . 2 = <*x1,x2,x3,x4*> . 2 by A3, FINSEQ_1:def 7
.= x2 by Th76 ;
:: thesis: ( p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
3 in dom <*x1,x2,x3,x4*> by A4, ENUMSET1:def 2;
hence p . 3 = <*x1,x2,x3,x4*> . 3 by A3, FINSEQ_1:def 7
.= x3 by Th76 ;
:: thesis: ( p . 4 = x4 & p . 5 = x5 )
4 in dom <*x1,x2,x3,x4*> by A4, ENUMSET1:def 2;
hence p . 4 = <*x1,x2,x3,x4*> . 4 by A3, FINSEQ_1:def 7
.= x4 by Th76 ;
:: thesis: p . 5 = x5
thus p . 5 = (<*x1,x2,x3,x4*> ^ <*x5*>) . (4 + 1) by A2, Th75
.= (<*x1,x2,x3,x4*> ^ <*x5*>) . ((len <*x1,x2,x3,x4*>) + 1) by Th76
.= <*x5*> . 1 by A1, FINSEQ_1:def 7
.= x5 by FINSEQ_1:def 8 ; :: thesis: verum
end;
assume that
A5: len p = 5 and
A6: p . 1 = x1 and
A7: p . 2 = x2 and
A8: p . 3 = x3 and
A9: p . 4 = x4 and
A10: p . 5 = x5 ; :: thesis: p = <*x1,x2,x3,x4,x5*>
A11: for k being Nat st k in dom <*x1,x2,x3,x4*> holds
p . k = <*x1,x2,x3,x4*> . k
proof
A12: len <*x1,x2,x3,x4*> = 4 by Th76;
let k be Nat; :: thesis: ( k in dom <*x1,x2,x3,x4*> implies p . k = <*x1,x2,x3,x4*> . k )
assume k in dom <*x1,x2,x3,x4*> ; :: thesis: p . k = <*x1,x2,x3,x4*> . k
then A13: k in {1,2,3,4} by A12, FINSEQ_1:def 3, FINSEQ_3:2;
per cases ( k = 1 or k = 2 or k = 3 or k = 4 ) by A13, ENUMSET1:def 2;
suppose k = 1 ; :: thesis: p . k = <*x1,x2,x3,x4*> . k
hence p . k = <*x1,x2,x3,x4*> . k by A6, Th76; :: thesis: verum
end;
suppose k = 2 ; :: thesis: p . k = <*x1,x2,x3,x4*> . k
hence p . k = <*x1,x2,x3,x4*> . k by A7, Th76; :: thesis: verum
end;
suppose k = 3 ; :: thesis: p . k = <*x1,x2,x3,x4*> . k
hence p . k = <*x1,x2,x3,x4*> . k by A8, Th76; :: thesis: verum
end;
suppose k = 4 ; :: thesis: p . k = <*x1,x2,x3,x4*> . k
hence p . k = <*x1,x2,x3,x4*> . k by A9, Th76; :: thesis: verum
end;
end;
end;
A14: for k being Nat st k in dom <*x5*> holds
p . ((len <*x1,x2,x3,x4*>) + k) = <*x5*> . k
proof
let k be Nat; :: thesis: ( k in dom <*x5*> implies p . ((len <*x1,x2,x3,x4*>) + k) = <*x5*> . k )
assume k in dom <*x5*> ; :: thesis: p . ((len <*x1,x2,x3,x4*>) + k) = <*x5*> . k
then k in {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then A15: k = 1 by TARSKI:def 1;
hence p . ((len <*x1,x2,x3,x4*>) + k) = p . (4 + 1) by Th76
.= <*x5*> . k by A10, A15, FINSEQ_1:def 8 ;
:: thesis: verum
end;
dom p = Seg (4 + 1) by A5, FINSEQ_1:def 3
.= Seg ((len <*x1,x2,x3,x4*>) + 1) by Th76
.= Seg ((len <*x1,x2,x3,x4*>) + (len <*x5*>)) by FINSEQ_1:39 ;
hence p = <*x1,x2,x3,x4*> ^ <*x5*> by A11, A14, FINSEQ_1:def 7
.= <*x1,x2,x3,x4,x5*> by Th75 ;
:: thesis: verum