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_{1}(m)
and

A6: dom g = card M and

A7: for m being set st m in card M holds

g . m = H_{1}(m)
; :: thesis: f = g

for x being object st x in dom f holds

f . x = g . x

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

A6: dom g = card M and

A7: for m being set st m in card M holds

g . m = H

for x being object st x in dom f holds

f . x = g . x

proof

hence
f = g
by A4, A6; :: thesis: verum
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_{1}(x)
by A4, A5, A8

.= g . x by A4, A7, A8 ; :: thesis: verum

end;assume A8: x in dom f ; :: thesis: f . x = g . x

thus f . x = H

.= g . x by A4, A7, A8 ; :: thesis: verum