let f, g be FinSequence; :: thesis: ( f in doms <*g*> iff ( len f = 1 & f . 1 in dom g ) )
set G = <*g*>;
A1: ( len <*g*> = 1 & <*g*> . 1 = g ) by FINSEQ_1:40;

hereby :: thesis: ( len f = 1 & f . 1 in dom g implies f in doms <*g*> )

assume A2: f in doms <*g*> ; :: thesis: ( len f = 1 & f . 1 in dom g )
then len f = 1 by A1, Th47;
then 1 in dom f by FINSEQ_3:25;
hence ( len f = 1 & f . 1 in dom g ) by A1, A2, Th47; :: thesis: verum

end;

assume A3: ( len f = 1 & f . 1 in dom g ) ; :: thesis: f in doms <*g*>

now :: thesis: for i being Nat st i in dom f holds
f . i in dom (<*g*> . i)

let i be Nat; :: thesis: ( i in dom f implies f . i in dom (<*g*> . i) )
assume A4: i in dom f ; :: thesis: f . i in dom (<*g*> . i)
( 1 <= i & i <= 1 ) by A3, A4, FINSEQ_3:25;
then i = 1 by XXREAL_0:1;
hence f . i in dom (<*g*> . i) by A3; :: thesis: verum

end;

hence f in doms <*g*> by A3, A1, Th47; :: thesis: verum