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
A26: dom x = (arity f1) -tuples_on [:A,B:] and
A27: for h being FinSequence of [:A,B:] st h in dom x holds
x . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] and
A28: dom y = (arity f1) -tuples_on [:A,B:] and
A29: 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

let c be Element of [:A,B:] * ; :: thesis: ( c in dom x implies x . c = y . c )
reconsider c' = c as FinSequence of [:A,B:] ;
assume c in dom x ; :: thesis: x . c = y . c
then ( x . c' = [(f1 . (pr1 c')),(f2 . (pr2 c'))] & y . c' = [(f1 . (pr1 c')),(f2 . (pr2 c'))] ) by A26, A27, A28, A29;
hence x . c = y . c ; :: thesis: verum

end;

hence x = y by A26, A28, PARTFUN1:34; :: thesis: verum