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