let R be non empty doubleLoopStr ; :: thesis: for x being Scalar of R
for f being FinSequence of R holds
( f = <*x*> iff ( len f = 1 & f /. 1 = x ) )
let x be Scalar of R; :: thesis: for f being FinSequence of R holds
( f = <*x*> iff ( len f = 1 & f /. 1 = x ) )
let f be FinSequence of R; :: thesis: ( f = <*x*> iff ( len f = 1 & f /. 1 = x ) )
thus ( f = <*x*> implies ( len f = 1 & f /. 1 = x ) ) by FINSEQ_1:40, FINSEQ_4:16; :: thesis: ( len f = 1 & f /. 1 = x implies f = <*x*> )
assume that
A1: len f = 1 and
A2: f /. 1 = x ; :: thesis: f = <*x*>
1 in dom f by A1, FINSEQ_3:25;
then f . 1 = x by A2, PARTFUN1:def 6;
hence f = <*x*> by A1, FINSEQ_1:40; :: thesis: verum