let x, y be non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:]; :: thesis: ( dom x = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom x holds

x . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) & dom y = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom y holds

y . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) implies x = y )

assume that

A25: dom x = (arity f1) -tuples_on [:A,B:] and

A26: for h being FinSequence of [:A,B:] st h in dom x holds

x . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] and

A27: dom y = (arity f1) -tuples_on [:A,B:] and

A28: for h being FinSequence of [:A,B:] st h in dom y holds

y . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ; :: thesis: x = y

x . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) & dom y = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom y holds

y . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) implies x = y )

assume that

A25: dom x = (arity f1) -tuples_on [:A,B:] and

A26: for h being FinSequence of [:A,B:] st h in dom x holds

x . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] and

A27: dom y = (arity f1) -tuples_on [:A,B:] and

A28: for h being FinSequence of [:A,B:] st h in dom y holds

y . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ; :: thesis: x = y

now :: thesis: for c being Element of [:A,B:] * st c in dom x holds

x . c = y . c

hence
x = y
by A25, A27, PARTFUN1:5; :: thesis: verumx . c = y . c

let c be Element of [:A,B:] * ; :: thesis: ( c in dom x implies x . c = y . c )

reconsider c9 = c as FinSequence of [:A,B:] ;

assume A29: c in dom x ; :: thesis: x . c = y . c

then x . c9 = [(f1 . (pr1 c9)),(f2 . (pr2 c9))] by A26;

hence x . c = y . c by A25, A27, A28, A29; :: thesis: verum

end;reconsider c9 = c as FinSequence of [:A,B:] ;

assume A29: c in dom x ; :: thesis: x . c = y . c

then x . c9 = [(f1 . (pr1 c9)),(f2 . (pr2 c9))] by A26;

hence x . c = y . c by A25, A27, A28, A29; :: thesis: verum