let X be non empty set ; :: thesis: for F being sequence of X
for n being Nat holds rng (F | (Segm (n + 1))) = (rng (F | (Segm n))) \/ {(F . n)}
let F be sequence of X; :: thesis: for n being Nat holds rng (F | (Segm (n + 1))) = (rng (F | (Segm n))) \/ {(F . n)}
let n be Nat; :: thesis: rng (F | (Segm (n + 1))) = (rng (F | (Segm n))) \/ {(F . n)}
now :: thesis: for y being object st y in rng (F | (Segm (n + 1))) holds
y in (rng (F | (Segm n))) \/ {(F . n)}
let y be object ; :: thesis: ( y in rng (F | (Segm (n + 1))) implies b1 in (rng (F | (Segm n))) \/ {(F . n)} )
assume y in rng (F | (Segm (n + 1))) ; :: thesis: b1 in (rng (F | (Segm n))) \/ {(F . n)}
then consider x being object such that
A1: ( x in dom (F | (Segm (n + 1))) & y = (F | (Segm (n + 1))) . x ) by FUNCT_1:def 3;
reconsider x = x as Nat by A1;
A4: y = F . x by A1, FUNCT_1:47;
x in (dom F) /\ (Segm (n + 1)) by A1, RELAT_1:61;
then A2: ( x in dom F & x in Segm (n + 1) ) by XBOOLE_0:def 4;
x < n + 1 by A2, NAT_1:44;
then A3: x <= n by NAT_1:13;
per cases ( x = n or x <> n ) ;
suppose x = n ; :: thesis: b1 in (rng (F | (Segm n))) \/ {(F . n)}
then y in {(F . n)} by A4, TARSKI:def 1;
hence y in (rng (F | (Segm n))) \/ {(F . n)} by XBOOLE_0:def 3; :: thesis: verum
end;
suppose x <> n ; :: thesis: b1 in (rng (F | (Segm n))) \/ {(F . n)}
then x < n by A3, XXREAL_0:1;
then x in Segm n by NAT_1:44;
then x in (dom F) /\ (Segm n) by A2, XBOOLE_0:def 4;
then x in dom (F | (Segm n)) by RELAT_1:61;
then ( (F | (Segm n)) . x in rng (F | (Segm n)) & (F | (Segm n)) . x = F . x ) by FUNCT_1:3, FUNCT_1:47;
hence y in (rng (F | (Segm n))) \/ {(F . n)} by A4, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
then A5: rng (F | (Segm (n + 1))) c= (rng (F | (Segm n))) \/ {(F . n)} by TARSKI:def 3;
now :: thesis: for y being object st y in (rng (F | (Segm n))) \/ {(F . n)} holds
y in rng (F | (Segm (n + 1)))
let y be object ; :: thesis: ( y in (rng (F | (Segm n))) \/ {(F . n)} implies b1 in rng (F | (Segm (n + 1))) )
assume A6: y in (rng (F | (Segm n))) \/ {(F . n)} ; :: thesis: b1 in rng (F | (Segm (n + 1)))
per cases ( y in rng (F | (Segm n)) or y in {(F . n)} ) by A6, XBOOLE_0:def 3;
suppose A7: y in rng (F | (Segm n)) ; :: thesis: b1 in rng (F | (Segm (n + 1)))
n <= n + 1 by NAT_1:11;
then F | (Segm n) c= F | (Segm (n + 1)) by NAT_1:39, RELAT_1:75;
then rng (F | (Segm n)) c= rng (F | (Segm (n + 1))) by RELAT_1:11;
hence y in rng (F | (Segm (n + 1))) by A7; :: thesis: verum
end;
suppose y in {(F . n)} ; :: thesis: b1 in rng (F | (Segm (n + 1)))
then A8: y = F . n by TARSKI:def 1;
n in NAT by ORDINAL1:def 12;
then ( n in dom F & n in Segm (n + 1) ) by FUNCT_2:def 1, NAT_1:45;
then n in (dom F) /\ (Segm (n + 1)) by XBOOLE_0:def 4;
then A9: n in dom (F | (Segm (n + 1))) by RELAT_1:61;
then F . n = (F | (Segm (n + 1))) . n by FUNCT_1:47;
hence y in rng (F | (Segm (n + 1))) by A8, A9, FUNCT_1:3; :: thesis: verum
end;
end;
end;
then (rng (F | (Segm n))) \/ {(F . n)} c= rng (F | (Segm (n + 1))) by TARSKI:def 3;
hence rng (F | (Segm (n + 1))) = (rng (F | (Segm n))) \/ {(F . n)} by A5, XBOOLE_0:def 10; :: thesis: verum