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 & (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) . 1 = x1 & (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) . 2 = x2 & (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) . 3 = x3 & (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) . 4 = x4 ) by Th87;
thus len p = (len (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>)) + (len <*x5*>) by A1, Th35
.= 4 + 1 by A2, Th57
.= 5 ; :: thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
dom (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) = Seg 4 by A2, Def3;
hence ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) by A1, A2, Def7, Lm7; :: thesis: p . 5 = x5
thus p . 5 = p . ((len (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>)) + 1) by A2
.= x5 by A1, Th59 ; :: thesis: verum