let i be Nat; :: thesis: for f being FinSequence of COMPLEX holds f = ((f | i) ^ ((f /^ i) | 1)) ^ (f /^ (i + 1))
let f be FinSequence of COMPLEX ; :: thesis: f = ((f | i) ^ ((f /^ i) | 1)) ^ (f /^ (i + 1))
f = (f | i) ^ (f /^ i) by RFINSEQ:8
.= (f | i) ^ (((f /^ i) | 1) ^ ((f /^ i) /^ 1)) by RFINSEQ:8
.= ((f | i) ^ ((f /^ i) | 1)) ^ ((f /^ i) /^ 1) by FINSEQ_1:32
.= ((f | i) ^ ((f /^ i) | 1)) ^ (f /^ (i + 1)) by FINSEQ681 ;
hence f = ((f | i) ^ ((f /^ i) | 1)) ^ (f /^ (i + 1)) ; :: thesis: verum