reconsider n = n as Element of NAT by ORDINAL1:def 12;
set f = (0,n) --> ((1. R),(1. R));
set q = (0_. R) +* ((0,n) --> ((1. R),(1. R)));
A2: dom ((0,n) --> ((1. R),(1. R))) = {0,n} by FUNCT_4:62;
A5: now :: thesis: for xx being object st xx in NAT holds
((0_. R) +* ((0,n) --> ((1. R),(1. R)))) . xx in the carrier of R
let xx be object ; :: thesis: ( xx in NAT implies ((0_. R) +* ((0,n) --> ((1. R),(1. R)))) . b1 in the carrier of R )
assume xx in NAT ; :: thesis: ((0_. R) +* ((0,n) --> ((1. R),(1. R)))) . b1 in the carrier of R
then reconsider x = xx as Element of NAT ;
per cases ( x = 0 or x = n or ( x <> 0 & x <> n ) ) ;
suppose x = 0 ; :: thesis: ((0_. R) +* ((0,n) --> ((1. R),(1. R)))) . b1 in the carrier of R
then ((0_. R) +* ((0,n) --> ((1. R),(1. R)))) . x = 1. R by Lm10;
hence ((0_. R) +* ((0,n) --> ((1. R),(1. R)))) . xx in the carrier of R ; :: thesis: verum
end;
suppose x = n ; :: thesis: ((0_. R) +* ((0,n) --> ((1. R),(1. R)))) . b1 in the carrier of R
then ((0_. R) +* ((0,n) --> ((1. R),(1. R)))) . x = 1. R by Lm10;
hence ((0_. R) +* ((0,n) --> ((1. R),(1. R)))) . xx in the carrier of R ; :: thesis: verum
end;
suppose ( x <> 0 & x <> n ) ; :: thesis: ((0_. R) +* ((0,n) --> ((1. R),(1. R)))) . b1 in the carrier of R
then ((0_. R) +* ((0,n) --> ((1. R),(1. R)))) . x = 0. R by Lm11;
hence ((0_. R) +* ((0,n) --> ((1. R),(1. R)))) . xx in the carrier of R ; :: thesis: verum
end;
end;
end;
dom (0_. R) = NAT by FUNCT_2:def 1;
then (dom (0_. R)) \/ (dom ((0,n) --> ((1. R),(1. R)))) = NAT by A2, XBOOLE_1:12;
then dom ((0_. R) +* ((0,n) --> ((1. R),(1. R)))) = NAT by FUNCT_4:def 1;
hence (0_. R) +* ((0,n) --> ((1. R),(1. R))) is sequence of R by A5, FUNCT_2:3; :: thesis: verum