let i, j be Nat; :: thesis: for x being set holds (i + j) |-> x = (i |-> x) ^ (j |-> x)
let x be set ; :: thesis: (i + j) |-> x = (i |-> x) ^ (j |-> x)
defpred S₁[ Nat] means (i + $1) |-> x = (i |-> x) ^ ($1 |-> x);
A1: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A2: (i + j) |-> x = (i |-> x) ^ (j |-> x) ; :: thesis: S₁[j + 1]
thus (i + (j + 1)) |-> x = ((i + j) + 1) |-> x
.= ((i + j) |-> x) ^ <*x*> by Th74
.= (i |-> x) ^ ((j |-> x) ^ <*x*>) by A2, FINSEQ_1:45
.= (i |-> x) ^ ((j + 1) |-> x) by Th74 ; :: thesis: verum

end;

(i + 0 ) |-> x = (i |-> x) ^ {} by FINSEQ_1:47
.= (i |-> x) ^ (0 |-> x) ;
then A3: S₁[ 0 ] ;
for j being Nat holds S₁[j] from NAT_1:sch 2(A3, A1);
hence (i + j) |-> x = (i |-> x) ^ (j |-> x) ; :: thesis: verum