let f be FinSequence; :: thesis: doms <*f*> = { <*i*> where i is Element of NAT : i in dom f }
thus doms <*f*> c= { <*i*> where i is Element of NAT : i in dom f } :: according to XBOOLE_0:def 10 :: thesis: { <*i*> where i is Element of NAT : i in dom f } c= doms <*f*>

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in doms <*f*> or y in { <*i*> where i is Element of NAT : i in dom f } )
assume A1: y in doms <*f*> ; :: thesis: y in { <*i*> where i is Element of NAT : i in dom f }
then reconsider y = y as FinSequence ;
A2: y . 1 in dom f by A1, Th51;
y = <*(y . 1)*> by A1, Th51, FINSEQ_1:40;
hence y in { <*i*> where i is Element of NAT : i in dom f } by A2; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { <*i*> where i is Element of NAT : i in dom f } or y in doms <*f*> )
assume y in { <*i*> where i is Element of NAT : i in dom f } ; :: thesis: y in doms <*f*>
then consider i being Element of NAT such that
A3: ( y = <*i*> & i in dom f ) ;
( len <*i*> = 1 & <*i*> . 1 = i ) by FINSEQ_1:40;
hence y in doms <*f*> by A3, Th51; :: thesis: verum