let n be Nat; :: thesis: for e being object holds (Segm (n + 1)) --> e = ((Segm n) --> e) ^ <%e%>
let e be object ; :: thesis: (Segm (n + 1)) --> e = ((Segm n) --> e) ^ <%e%>
set p = (Segm n) --> e;
set q = (Segm (n + 1)) --> e;
A2: dom ((Segm (n + 1)) --> e) = n + 1
.= (len ((Segm n) --> e)) + (len <%e%>) by Th31 ;
A3: for k being Nat st k in dom ((Segm n) --> e) holds
((Segm (n + 1)) --> e) . k = ((Segm n) --> e) . k

proof

let k be Nat; :: thesis: ( k in dom ((Segm n) --> e) implies ((Segm (n + 1)) --> e) . k = ((Segm n) --> e) . k )
assume A4: k in dom ((Segm n) --> e) ; :: thesis: ((Segm (n + 1)) --> e) . k = ((Segm n) --> e) . k
(Segm n) --> e c= (Segm (n + 1)) --> e by FUNCT_4:4, NAT_1:63;
hence ((Segm (n + 1)) --> e) . k = ((Segm n) --> e) . k by A4, GRFUNC_1:2; :: thesis: verum

end;

for k being Nat st k in dom <%e%> holds
((Segm (n + 1)) --> e) . ((len ((Segm n) --> e)) + k) = <%e%> . k

proof

let k be Nat; :: thesis: ( k in dom <%e%> implies ((Segm (n + 1)) --> e) . ((len ((Segm n) --> e)) + k) = <%e%> . k )
assume A5: k in dom <%e%> ; :: thesis: ((Segm (n + 1)) --> e) . ((len ((Segm n) --> e)) + k) = <%e%> . k
A6: k = 0 by A5, TARSKI:def 1;
len ((Segm n) --> e) < n + 1 by NAT_1:13;
then (len ((Segm n) --> e)) + 0 in Segm (n + 1) by NAT_1:44;
hence ((Segm (n + 1)) --> e) . ((len ((Segm n) --> e)) + k) = <%e%> . k by A6, FUNCOP_1:7; :: thesis: verum

end;

hence (Segm (n + 1)) --> e = ((Segm n) --> e) ^ <%e%> by A2, A3, Def3; :: thesis: verum