let f, g be T-Sequence of NAT ; :: thesis: ( dom f = card M & ( for m being set st m in card M holds
f . m = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S))) . m) ) & dom g = card M & ( for m being set st m in card M holds
g . m = il. S,((canonical_isomorphism_of (RelIncl (order_type_of (RelIncl (LocNums M,S)))),(RelIncl (LocNums M,S))) . m) ) implies f = g )
assume that
A4: dom f = card M and
A5: for m being set st m in card M holds
f . m = H₁(m) and
A6: dom g = card M and
A7: for m being set st m in card M holds
g . m = H₁(m) ; :: thesis: f = g
for x being set st x in dom f holds
f . x = g . x

proof

let x be set ; :: thesis: ( x in dom f implies f . x = g . x )
assume A8: x in dom f ; :: thesis: f . x = g . x
thus f . x = H₁(x) by A4, A5, A8
.= g . x by A4, A7, A8 ; :: thesis: verum

end;

hence f = g by A4, A6, FUNCT_1:9; :: thesis: verum