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