let i, j be natural Number ; :: thesis: for x being object holds (i + j) |-> x = (i |-> x) ^ (j |-> x)
let x be object ; :: thesis: (i + j) |-> x = (i |-> x) ^ (j |-> x)
A0: j is Nat by TARSKI:1;
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 Th58
.= (i |-> x) ^ ((j |-> x) ^ <*x*>) by A2, FINSEQ_1:32
.= (i |-> x) ^ ((j + 1) |-> x) by Th58 ; :: thesis: verum

end;

(i + 0) |-> x = (i |-> x) ^ {} by FINSEQ_1:34
.= (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) by A0; :: thesis: verum