let I be non empty set ; :: thesis: for X being ManySortedSet of I
for l1, l2 being Element of I
for i1, i2 being set holds X +* ((l1,l2) --> (i1,i2)) = (X +* (l1,i1)) +* (l2,i2)
let X be ManySortedSet of I; :: thesis: for l1, l2 being Element of I
for i1, i2 being set holds X +* ((l1,l2) --> (i1,i2)) = (X +* (l1,i1)) +* (l2,i2)
let l1, l2 be Element of I; :: thesis: for i1, i2 being set holds X +* ((l1,l2) --> (i1,i2)) = (X +* (l1,i1)) +* (l2,i2)
let i1, i2 be set ; :: thesis: X +* ((l1,l2) --> (i1,i2)) = (X +* (l1,i1)) +* (l2,i2)
A1: dom X = I by PARTFUN1:def 2;
then A2: l1 in dom X ;
dom (X +* (l1,i1)) = I by A1, Th29;
then A3: l2 in dom (X +* (l1,i1)) ;
thus X +* ((l1,l2) --> (i1,i2)) = X +* ((l1 .--> i1) +* (l2 .--> i2))
.= (X +* (l1 .--> i1)) +* (l2 .--> i2) by FUNCT_4:14
.= (X +* (l1,i1)) +* (l2 .--> i2) by A2, Def2
.= (X +* (l1,i1)) +* (l2,i2) by A3, Def2 ; :: thesis: verum