let n, m be Nat; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L ex q being Polynomial of (n + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for x being Function of n,L
for y being Function of (n + m),L st y | n = x holds
eval (p,x) = eval (q,y) ) )
let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of n,L ex q being Polynomial of (n + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for x being Function of n,L
for y being Function of (n + m),L st y | n = x holds
eval (p,x) = eval (q,y) ) )
let p be Polynomial of n,L; :: thesis: ex q being Polynomial of (n + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for x being Function of n,L
for y being Function of (n + m),L st y | n = x holds
eval (p,x) = eval (q,y) ) )
defpred S₁[ Nat] means ex q being Polynomial of (n + $1),L st
( rng q c= (rng p) \/ {(0. L)} & ( for x being Function of n,L
for y being Function of (n + $1),L st y | n = x holds
eval (p,x) = eval (q,y) ) );
A1: S₁[ 0 ]

proof

reconsider q = p as Polynomial of (n + 0),L ;
take q ; :: thesis: ( rng q c= (rng p) \/ {(0. L)} & ( for x being Function of n,L
for y being Function of (n + 0),L st y | n = x holds
eval (p,x) = eval (q,y) ) )
thus rng q c= (rng p) \/ {(0. L)} by XBOOLE_1:7; :: thesis: for x being Function of n,L
for y being Function of (n + 0),L st y | n = x holds
eval (p,x) = eval (q,y)
thus for x being Function of n,L
for y being Function of (n + 0),L st y | n = x holds
eval (p,x) = eval (q,y) ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
set k1 = k + 1;
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider q being Polynomial of (n + k),L such that
A3: rng q c= (rng p) \/ {(0. L)} and
A4: for x being Function of n,L
for y being Function of (n + k),L st y | n = x holds
eval (p,x) = eval (q,y) ;
reconsider P = q extended_by_0 as Polynomial of (n + (k + 1)),L ;
take P ; :: thesis: ( rng P c= (rng p) \/ {(0. L)} & ( for x being Function of n,L
for y being Function of (n + (k + 1)),L st y | n = x holds
eval (p,x) = eval (P,y) ) )
rng P = (rng q) \/ {(0. L)} by Th10;
then rng P c= ((rng p) \/ {(0. L)}) \/ {(0. L)} by A3, XBOOLE_1:13;
hence rng P c= (rng p) \/ {(0. L)} by XBOOLE_1:7, XBOOLE_1:12; :: thesis: for x being Function of n,L
for y being Function of (n + (k + 1)),L st y | n = x holds
eval (p,x) = eval (P,y)
let x be Function of n,L; :: thesis: for y being Function of (n + (k + 1)),L st y | n = x holds
eval (p,x) = eval (P,y)
let y be Function of (n + (k + 1)),L; :: thesis: ( y | n = x implies eval (p,x) = eval (P,y) )
assume A5: y | n = x ; :: thesis: eval (p,x) = eval (P,y)
A6: ( rng (y | (n + k)) c= rng y & rng y c= the carrier of L ) by RELAT_1:70;
( len (@ y) = n + (k + 1) & n + k < (n + k) + 1 ) by CARD_1:def 7, NAT_1:13;
then len ((@ y) | (n + k)) = n + k by AFINSQ_1:54;
then reconsider Y = (@ y) | (n + k) as Function of (n + k),L by A6, FUNCT_2:2;
Segm n c= Segm (n + k) by NAT_1:39, NAT_1:11;
then A7: Y | n = x by A5, RELAT_1:74;
thus eval (P,y) = eval (q,Y) by Th18
.= eval (p,x) by A4, A7 ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence ex q being Polynomial of (n + m),L st
( rng q c= (rng p) \/ {(0. L)} & ( for x being Function of n,L
for y being Function of (n + m),L st y | n = x holds
eval (p,x) = eval (q,y) ) ) ; :: thesis: verum