let F, G be ManySortedSet of NATPLUS ; :: thesis: ( ( for n being non zero Nat holds F . n = n (#) f ) & ( for n being non zero Nat holds G . n = n (#) f ) implies F = G )
assume that
A3: for n being non zero Nat holds F . n = n (#) f and
A4: for n being non zero Nat holds G . n = n (#) f ; :: thesis: F = G
dom F = NATPLUS by PARTFUN1:def 2;
hence dom F = dom G by PARTFUN1:def 2; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in proj1 F or F . b₁ = G . b₁ )
let n be object ; :: thesis: ( not n in proj1 F or F . n = G . n )
assume n in dom F ; :: thesis: F . n = G . n
then reconsider m = n as Element of NATPLUS ;
thus F . n = m (#) f by A3
.= G . n by A4 ; :: thesis: verum