let v be object ; :: thesis: for V, A being set
for d being TypeSCNominativeData of V,A
for f being SCBinominativeFunction of V,A holds rng (NDdataSeq (<*f*>,<*v*>,d)) = v .--> (f . d)
let V, A be set ; :: thesis: for d being TypeSCNominativeData of V,A
for f being SCBinominativeFunction of V,A holds rng (NDdataSeq (<*f*>,<*v*>,d)) = v .--> (f . d)
let d be TypeSCNominativeData of V,A; :: thesis: for f being SCBinominativeFunction of V,A holds rng (NDdataSeq (<*f*>,<*v*>,d)) = v .--> (f . d)
let f be SCBinominativeFunction of V,A; :: thesis: rng (NDdataSeq (<*f*>,<*v*>,d)) = v .--> (f . d)
set g = <*f*>;
set X = <*v*>;
set N = NDdataSeq (<*f*>,<*v*>,d);
set F = v .--> (f . d);
A1: dom (NDdataSeq (<*f*>,<*v*>,d)) = dom <*v*> by Def4;
A2: dom <*v*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
A5: v .--> (f . d) = {[v,(f . d)]} by ZFMISC_1:29;
thus rng (NDdataSeq (<*f*>,<*v*>,d)) c= v .--> (f . d) :: according to XBOOLE_0:def 10 :: thesis: v .--> (f . d) c= rng (NDdataSeq (<*f*>,<*v*>,d))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (NDdataSeq (<*f*>,<*v*>,d)) or y in v .--> (f . d) )
assume y in rng (NDdataSeq (<*f*>,<*v*>,d)) ; :: thesis: y in v .--> (f . d)
then consider z being object such that
A6: z in dom (NDdataSeq (<*f*>,<*v*>,d)) and
A7: (NDdataSeq (<*f*>,<*v*>,d)) . z = y by FUNCT_1:def 3;
A8: z = 1 by A1, A2, A6, TARSKI:def 1;
(NDdataSeq (<*f*>,<*v*>,d)) . z = [(<*v*> . z),((<*f*> . z) . d)] by A1, A6, Def4;
hence y in v .--> (f . d) by A7, A8, A5, TARSKI:def 1; :: thesis: verum

end;

let m, n be object ; :: according to RELAT_1:def 3 :: thesis: ( not [m,n] in v .--> (f . d) or [m,n] in rng (NDdataSeq (<*f*>,<*v*>,d)) )
assume [m,n] in v .--> (f . d) ; :: thesis: [m,n] in rng (NDdataSeq (<*f*>,<*v*>,d))
then A9: [m,n] = [v,(f . d)] by A5, TARSKI:def 1;
A10: 1 in dom (NDdataSeq (<*f*>,<*v*>,d)) by A1, A2, TARSKI:def 1;
then (NDdataSeq (<*f*>,<*v*>,d)) . 1 = [(<*v*> . 1),((<*f*> . 1) . d)] by A1, Def4;
hence [m,n] in rng (NDdataSeq (<*f*>,<*v*>,d)) by A9, A10, FUNCT_1:def 3; :: thesis: verum