let n be Nat; :: thesis: for b being bag of n
for L being non trivial well-unital doubleLoopStr
for x being Function of n,L
for y being Function of (n + 1),L st y | n = x holds
eval (b,x) = eval ((b bag_extend 0),y)
let b be bag of n; :: thesis: for L being non trivial well-unital doubleLoopStr
for x being Function of n,L
for y being Function of (n + 1),L st y | n = x holds
eval (b,x) = eval ((b bag_extend 0),y)
let L be non trivial well-unital doubleLoopStr ; :: thesis: for x being Function of n,L
for y being Function of (n + 1),L st y | n = x holds
eval (b,x) = eval ((b bag_extend 0),y)
let x be Function of n,L; :: thesis: for y being Function of (n + 1),L st y | n = x holds
eval (b,x) = eval ((b bag_extend 0),y)
let y be Function of (n + 1),L; :: thesis: ( y | n = x implies eval (b,x) = eval ((b bag_extend 0),y) )
assume A1: y | n = x ; :: thesis: eval (b,x) = eval ((b bag_extend 0),y)
set S = SgmX ((RelIncl n),(support b));
set B = b bag_extend 0;
set S1 = SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)));
consider P being FinSequence of L such that
A2: ( len P = len (SgmX ((RelIncl n),(support b))) & eval (b,x) = Product P ) and
A3: for i being Element of NAT st 1 <= i & i <= len P holds
P /. i = (power L) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) by POLYNOM2:def 2;
consider P1 being FinSequence of L such that
A4: ( len P1 = len (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0)))) & eval ((b bag_extend 0),y) = Product P1 ) and
A5: for i being Element of NAT st 1 <= i & i <= len P1 holds
P1 /. i = (power L) . (((y * (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0))))) /. i),(((b bag_extend 0) * (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0))))) /. i)) by POLYNOM2:def 2;
A6: SgmX ((RelIncl n),(support b)) = SgmX ((RelIncl (n + 1)),(support (b bag_extend 0))) by Th12;
A7: rng (SgmX ((RelIncl n),(support b))) c= n ;
A8: y * (SgmX ((RelIncl n),(support b))) = y * ((id n) * (SgmX ((RelIncl n),(support b)))) by A7, RELAT_1:53
.= (y * (id n)) * (SgmX ((RelIncl n),(support b))) by RELAT_1:36
.= x * (SgmX ((RelIncl n),(support b))) by RELAT_1:65, A1 ;
A9: b = (0,n) -cut (b bag_extend 0) by Th5
.= (b bag_extend 0) | n by NAT_1:11, Th3 ;
A10: (b bag_extend 0) * (SgmX ((RelIncl n),(support b))) = (b bag_extend 0) * ((id n) * (SgmX ((RelIncl n),(support b)))) by A7, RELAT_1:53
.= ((b bag_extend 0) * (id n)) * (SgmX ((RelIncl n),(support b))) by RELAT_1:36
.= b * (SgmX ((RelIncl n),(support b))) by A9, RELAT_1:65 ;
for i being Nat st 1 <= i & i <= len P holds
P . i = P1 . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len P implies P . i = P1 . i )
assume A11: ( 1 <= i & i <= len P ) ; :: thesis: P . i = P1 . i
reconsider I = i as Element of NAT by ORDINAL1:def 12;
A12: ( i in dom P & i in dom P1 ) by A2, A4, A6, A11, FINSEQ_3:25;
then P /. I = P . i by PARTFUN1:def 6;
hence P . i = (power L) . (((y * (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0))))) /. i),(((b bag_extend 0) * (SgmX ((RelIncl (n + 1)),(support (b bag_extend 0))))) /. i)) by A3, A11, A6, A8, A10
.= P1 /. I by A5, A11, A2, A4, A6
.= P1 . i by A12, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence eval (b,x) = eval ((b bag_extend 0),y) by A2, A4, A6, FINSEQ_1:14; :: thesis: verum