let v be object ; 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 ; 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; for f being SCBinominativeFunction of V,A holds rng (NDdataSeq (<*f*>,<*v*>,d)) = v .--> (f . d)
let f be SCBinominativeFunction of V,A; 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;
A3:
<*v*> . 1 = v
by FINSEQ_1:40;
A4:
<*f*> . 1 = f
by FINSEQ_1:40;
A5:
v .--> (f . d) = {[v,(f . d)]}
by ZFMISC_1:29;
thus
rng (NDdataSeq (<*f*>,<*v*>,d)) c= v .--> (f . d)
XBOOLE_0:def 10 v .--> (f . d) c= rng (NDdataSeq (<*f*>,<*v*>,d))proof
let y be
object ;
TARSKI:def 3 ( not y in rng (NDdataSeq (<*f*>,<*v*>,d)) or y in v .--> (f . d) )
assume
y in rng (NDdataSeq (<*f*>,<*v*>,d))
;
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 A3, A4, A7, A8, A5, TARSKI:def 1;
verum
end;
let m, n be object ; RELAT_1:def 3 ( not [m,n] in v .--> (f . d) or [m,n] in rng (NDdataSeq (<*f*>,<*v*>,d)) )
assume
[m,n] in v .--> (f . d)
; [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 A3, A4, A9, A10, FUNCT_1:def 3; verum