let R be non empty doubleLoopStr ; :: thesis: for x being Scalar of R
for f being FinSequence of R holds (f ^ <*x*>) /. ((len f) + 1) = x
let x be Scalar of R; :: thesis: for f being FinSequence of R holds (f ^ <*x*>) /. ((len f) + 1) = x
let f be FinSequence of R; :: thesis: (f ^ <*x*>) /. ((len f) + 1) = x
A1: 1 <= (len f) + 1 by NAT_1:11;
(len f) + 1 = (len f) + (len <*x*>) by FINSEQ_1:39
.= len (f ^ <*x*>) by FINSEQ_1:22 ;
then (len f) + 1 in dom (f ^ <*x*>) by A1, FINSEQ_3:25;
then (f ^ <*x*>) /. ((len f) + 1) = (f ^ <*x*>) . ((len f) + 1) by PARTFUN1:def 6
.= x by FINSEQ_1:42 ;
hence (f ^ <*x*>) /. ((len f) + 1) = x ; :: thesis: verum