let p1, p2 be PFuncFinSequence of A; :: thesis: ( dom p1 = dom the charact of U0 & ( for n being set

for o being operation of U0 st n in dom p1 & o = the charact of U0 . n holds

p1 . n = o /. A ) & dom p2 = dom the charact of U0 & ( for n being set

for o being operation of U0 st n in dom p2 & o = the charact of U0 . n holds

p2 . n = o /. A ) implies p1 = p2 )

assume that

A4: dom p1 = dom the charact of U0 and

A5: for n being set

for o being operation of U0 st n in dom p1 & o = the charact of U0 . n holds

p1 . n = o /. A and

A6: dom p2 = dom the charact of U0 and

A7: for n being set

for o being operation of U0 st n in dom p2 & o = the charact of U0 . n holds

p2 . n = o /. A ; :: thesis: p1 = p2

for n being Nat st n in dom the charact of U0 holds

p1 . n = p2 . n

for o being operation of U0 st n in dom p1 & o = the charact of U0 . n holds

p1 . n = o /. A ) & dom p2 = dom the charact of U0 & ( for n being set

for o being operation of U0 st n in dom p2 & o = the charact of U0 . n holds

p2 . n = o /. A ) implies p1 = p2 )

assume that

A4: dom p1 = dom the charact of U0 and

A5: for n being set

for o being operation of U0 st n in dom p1 & o = the charact of U0 . n holds

p1 . n = o /. A and

A6: dom p2 = dom the charact of U0 and

A7: for n being set

for o being operation of U0 st n in dom p2 & o = the charact of U0 . n holds

p2 . n = o /. A ; :: thesis: p1 = p2

for n being Nat st n in dom the charact of U0 holds

p1 . n = p2 . n

proof

hence
p1 = p2
by A4, A6, FINSEQ_1:13; :: thesis: verum
let n be Nat; :: thesis: ( n in dom the charact of U0 implies p1 . n = p2 . n )

assume A8: n in dom the charact of U0 ; :: thesis: p1 . n = p2 . n

then reconsider k = the charact of U0 . n as operation of U0 by FUNCT_1:def 3;

p1 . n = k /. A by A4, A5, A8;

hence p1 . n = p2 . n by A6, A7, A8; :: thesis: verum

end;assume A8: n in dom the charact of U0 ; :: thesis: p1 . n = p2 . n

then reconsider k = the charact of U0 . n as operation of U0 by FUNCT_1:def 3;

p1 . n = k /. A by A4, A5, A8;

hence p1 . n = p2 . n by A6, A7, A8; :: thesis: verum