let O, E1, E2 be set ; :: thesis: for A1 being Action of O,E1
for A2 being Action of O,E2
for F being FinSequence of O st E1 c= E2 & ( for o being Element of O
for f1 being Function of E1,E1
for f2 being Function of E2,E2 st f1 = A1 . o & f2 = A2 . o holds
f1 = f2 | E1 ) holds
Product (F,A1) = (Product (F,A2)) | E1
let A1 be Action of O,E1; :: thesis: for A2 being Action of O,E2
for F being FinSequence of O st E1 c= E2 & ( for o being Element of O
for f1 being Function of E1,E1
for f2 being Function of E2,E2 st f1 = A1 . o & f2 = A2 . o holds
f1 = f2 | E1 ) holds
Product (F,A1) = (Product (F,A2)) | E1
let A2 be Action of O,E2; :: thesis: for F being FinSequence of O st E1 c= E2 & ( for o being Element of O
for f1 being Function of E1,E1
for f2 being Function of E2,E2 st f1 = A1 . o & f2 = A2 . o holds
f1 = f2 | E1 ) holds
Product (F,A1) = (Product (F,A2)) | E1
let F be FinSequence of O; :: thesis: ( E1 c= E2 & ( for o being Element of O
for f1 being Function of E1,E1
for f2 being Function of E2,E2 st f1 = A1 . o & f2 = A2 . o holds
f1 = f2 | E1 ) implies Product (F,A1) = (Product (F,A2)) | E1 )
defpred S₁[ Nat] means for F being FinSequence of O st len F = $1 holds
Product (F,A1) = (Product (F,A2)) | E1;
assume A1: E1 c= E2 ; :: thesis: ( ex o being Element of O ex f1 being Function of E1,E1 ex f2 being Function of E2,E2 st
( f1 = A1 . o & f2 = A2 . o & not f1 = f2 | E1 ) or Product (F,A1) = (Product (F,A2)) | E1 )
A2: S₁[ 0 ]

proof

let F be FinSequence of O; :: thesis: ( len F = 0 implies Product (F,A1) = (Product (F,A2)) | E1 )

A3: now :: thesis: for x being object st x in dom (id E1) holds
(id E1) . x = (id E2) . x

let x be object ; :: thesis: ( x in dom (id E1) implies (id E1) . x = (id E2) . x )
assume A4: x in dom (id E1) ; :: thesis: (id E1) . x = (id E2) . x
then A5: x in E1 ;
thus (id E1) . x = x by A4, FUNCT_1:18
.= (id E2) . x by A1, A5, FUNCT_1:18 ; :: thesis: verum

end;

E1 = E2 /\ E1 by A1, XBOOLE_1:28;
then dom (id E1) = E2 /\ E1 ;
then A6: dom (id E1) = (dom (id E2)) /\ E1 ;
assume A7: len F = 0 ; :: thesis: Product (F,A1) = (Product (F,A2)) | E1
hence Product (F,A1) = id E1 by Def3
.= (id E2) | E1 by A6, A3, FUNCT_1:46
.= (Product (F,A2)) | E1 by A7, Def3 ;
:: thesis: verum

end;

assume A8: for o being Element of O
for f1 being Function of E1,E1
for f2 being Function of E2,E2 st f1 = A1 . o & f2 = A2 . o holds
f1 = f2 | E1 ; :: thesis: Product (F,A1) = (Product (F,A2)) | E1

per cases ( O is empty or not O is empty ) ;

suppose O is empty ; :: thesis: Product (F,A1) = (Product (F,A2)) | E1

then len F = 0 ;
hence Product (F,A1) = (Product (F,A2)) | E1 by A2; :: thesis: verum

end;

suppose A9: not O is empty ; :: thesis: Product (F,A1) = (Product (F,A2)) | E1

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A11: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for F being FinSequence of O st len F = k + 1 holds
Product (F,A1) = (Product (F,A2)) | E1

let F be FinSequence of O; :: thesis: ( len F = k + 1 implies Product (F,A1) = (Product (F,A2)) | E1 )
assume A12: len F = k + 1 ; :: thesis: Product (F,A1) = (Product (F,A2)) | E1
then consider Fk being FinSequence of O, o being Element of O such that
A13: F = Fk ^ <*o*> by FINSEQ_2:19;
len F = (len Fk) + (len <*o*>) by A13, FINSEQ_1:22;
then A14: k + 1 = (len Fk) + 1 by A12, FINSEQ_1:39;

A15: now :: thesis: for x being object st x in dom (Product (F,A1)) holds
(Product (F,A1)) . x = ((Product (F,A2)) | E1) . x

{o} c= O by A9, ZFMISC_1:31;
then rng <*o*> c= O by FINSEQ_1:38;
then reconsider Fo = <*o*> as FinSequence of O by FINSEQ_1:def 4;
let x be object ; :: thesis: ( x in dom (Product (F,A1)) implies (Product (F,A1)) . x = ((Product (F,A2)) | E1) . x )
assume A16: x in dom (Product (F,A1)) ; :: thesis: (Product (F,A1)) . x = ((Product (F,A2)) | E1) . x
then A17: x in E1 ;
A18: o in O by A9;
then o in dom A1 by FUNCT_2:def 1;
then A1 . o in rng A1 by FUNCT_1:3;
then consider f1 being Function such that
A19: f1 = A1 . o and
A20: dom f1 = E1 and
A21: rng f1 c= E1 by FUNCT_2:def 2;
A22: Product (Fo,A1) = f1 by A9, A19, Lm25;
o in dom A2 by A18, FUNCT_2:def 1;
then A2 . o in rng A2 by FUNCT_1:3;
then consider f2 being Function such that
A23: f2 = A2 . o and
A24: dom f2 = E2 and
rng f2 c= E2 by FUNCT_2:def 2;
A25: Product (Fo,A2) = f2 by A9, A23, Lm25;
A26: f1 . x in rng f1 by A16, A20, FUNCT_1:3;
A27: Product (F,A2) = (Product (Fk,A2)) * (Product (Fo,A2)) by A9, A13, Lm28
.= (Product (Fk,A2)) * f2 by A9, A23, Lm25 ;
Product (F,A1) = (Product (Fk,A1)) * (Product (Fo,A1)) by A9, A13, Lm28
.= (Product (Fk,A1)) * f1 by A9, A19, Lm25 ;
hence (Product (F,A1)) . x = (Product (Fk,A1)) . (f1 . x) by A16, A20, FUNCT_1:13
.= ((Product (Fk,A2)) | E1) . (f1 . x) by A11, A14
.= (Product (Fk,A2)) . (f1 . x) by A21, A26, FUNCT_1:49
.= (Product (Fk,A2)) . ((f2 | E1) . x) by A8, A19, A23, A22, A25
.= (Product (Fk,A2)) . (f2 . x) by A16, FUNCT_1:49
.= ((Product (Fk,A2)) * f2) . x by A1, A17, A24, FUNCT_1:13
.= ((Product (F,A2)) | E1) . x by A16, A27, FUNCT_1:49 ;
:: thesis: verum

end;

Product (F,A2) in Funcs (E2,E2) by FUNCT_2:9;
then ex f2 being Function st
( Product (F,A2) = f2 & dom f2 = E2 & rng f2 c= E2 ) by FUNCT_2:def 2;
then A28: dom ((Product (F,A2)) | E1) = E2 /\ E1 by RELAT_1:61
.= E1 by A1, XBOOLE_1:28 ;
Product (F,A1) in Funcs (E1,E1) by FUNCT_2:9;
then ex f1 being Function st
( Product (F,A1) = f1 & dom f1 = E1 & rng f1 c= E1 ) by FUNCT_2:def 2;
hence Product (F,A1) = (Product (F,A2)) | E1 by A28, A15, FUNCT_1:2; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A29: for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A10);
reconsider k = len F as Element of NAT ;
k = len F ;
hence Product (F,A1) = (Product (F,A2)) | E1 by A29; :: thesis: verum

end;

end;