let IT1, IT2 be Function of ((D *) \ {{}}),D; :: thesis: ( ( for x being Element of (D *) \ {{}} holds IT1 . x = (MultPlace (f,x)) . ((len x) - 1) ) & ( for x being Element of (D *) \ {{}} holds IT2 . x = (MultPlace (f,x)) . ((len x) - 1) ) implies IT1 = IT2 )
A4: ( dom IT1 = (D *) \ {{}} & dom IT2 = (D *) \ {{}} ) by FUNCT_2:def 1;
assume A5: for x being Element of (D *) \ {{}} holds IT1 . x = (MultPlace (f,x)) . ((len x) - 1) ; :: thesis: ( ex x being Element of (D *) \ {{}} st not IT2 . x = (MultPlace (f,x)) . ((len x) - 1) or IT1 = IT2 )
assume A6: for x being Element of (D *) \ {{}} holds IT2 . x = (MultPlace (f,x)) . ((len x) - 1) ; :: thesis: IT1 = IT2

now :: thesis: for x being object st x in dom IT1 holds
IT1 . x = IT2 . x

let x be object ; :: thesis: ( x in dom IT1 implies IT1 . x = IT2 . x )
assume x in dom IT1 ; :: thesis: IT1 . x = IT2 . x
then reconsider xx = x as Element of (D *) \ {{}} ;
IT1 . x = (MultPlace (f,xx)) . ((len xx) - 1) by A5
.= IT2 . x by A6 ;
hence IT1 . x = IT2 . x ; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_1:2, A4; :: thesis: verum