let x1, x2, x3, x4 be set ; :: thesis: for p being FinSequence st p = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> holds
( 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*> implies ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) )
assume A1: p = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> ; :: thesis: ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
set p13 = (<*x1*> ^ <*x2*>) ^ <*x3*>;
A2: (<*x1*> ^ <*x2*>) ^ <*x3*> = <*x1,x2,x3*> ;
then A3: len ((<*x1*> ^ <*x2*>) ^ <*x3*>) = 3 by Th45;
A4: ( ((<*x1*> ^ <*x2*>) ^ <*x3*>) . 1 = x1 & ((<*x1*> ^ <*x2*>) ^ <*x3*>) . 2 = x2 ) by A2;
A5: ((<*x1*> ^ <*x2*>) ^ <*x3*>) . 3 = x3 by A2;
thus len p = (len ((<*x1*> ^ <*x2*>) ^ <*x3*>)) + (len <*x4*>) by A1, Th22
.= 3 + 1 by A3, Th40
.= 4 ; :: thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
A6: dom ((<*x1*> ^ <*x2*>) ^ <*x3*>) = Seg 3 by A3, Def3;
1 in Seg 3 & ... & 3 in Seg 3 ;
hence ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 ) by A1, A4, A5, Def7, A6; :: thesis: p . 4 = x4
thus p . 4 = p . ((len ((<*x1*> ^ <*x2*>) ^ <*x3*>)) + 1) by A3
.= x4 by A1, Th42 ; :: thesis: verum