let I be 2 -element set ; :: thesis: for f being ManySortedSet of I
for i, j being Element of I
for x being object st i <> j holds
f +* (i,x) = (i,j) --> (x,(f . j))

let f be ManySortedSet of I; :: thesis: for i, j being Element of I
for x being object st i <> j holds
f +* (i,x) = (i,j) --> (x,(f . j))

let i, j be Element of I; :: thesis: for x being object st i <> j holds
f +* (i,x) = (i,j) --> (x,(f . j))

let x be object ; :: thesis: ( i <> j implies f +* (i,x) = (i,j) --> (x,(f . j)) )
assume A1: i <> j ; :: thesis: f +* (i,x) = (i,j) --> (x,(f . j))
then a2: I = {i,j} by Th8;
then A2: dom f = {i,j} by PARTFUN1:def 2;
A3: dom (f +* (i,x)) = dom f by FUNCT_7:30
.= dom ((i,j) --> (x,(f . j))) by ;
for z being object st z in dom (f +* (i,x)) holds
(f +* (i,x)) . z = ((i,j) --> (x,(f . j))) . z
proof
let z be object ; :: thesis: ( z in dom (f +* (i,x)) implies (f +* (i,x)) . z = ((i,j) --> (x,(f . j))) . z )
assume z in dom (f +* (i,x)) ; :: thesis: (f +* (i,x)) . z = ((i,j) --> (x,(f . j))) . z
per cases then ( z = i or z = j ) by ;
suppose A5: z = i ; :: thesis: (f +* (i,x)) . z = ((i,j) --> (x,(f . j))) . z
hence (f +* (i,x)) . z = x by
.= ((i,j) --> (x,(f . j))) . z by ;
:: thesis: verum
end;
suppose A6: z = j ; :: thesis: (f +* (i,x)) . z = ((i,j) --> (x,(f . j))) . z
hence (f +* (i,x)) . z = f . j by
.= ((i,j) --> (x,(f . j))) . z by ;
:: thesis: verum
end;
end;
end;
hence f +* (i,x) = (i,j) --> (x,(f . j)) by ; :: thesis: verum