let f, g be Sequence of NAT ; :: thesis: ( dom f = card M & ( for m being set st m in card M holds
f . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) & dom g = card M & ( for m being set st m in card M holds
g . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . 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 object st x in dom f holds
f . x = g . x

proof

let x be object ; :: 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; :: thesis: verum