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_{1}[ 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_{1}[ 0 ]

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

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

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

proof

assume A8:
for o being Element of O
let F be FinSequence of O; :: thesis: ( len F = 0 implies Product (F,A1) = (Product (F,A2)) | E1 )

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;A3: now :: thesis: for x being object st x in dom (id E1) holds

(id E1) . x = (id E2) . x

E1 = E2 /\ E1
by A1, XBOOLE_1:28;(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;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

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

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 )
;

end;

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

A10:
for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[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;S

proof

A29:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A11: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A11: S

now :: thesis: for F being FinSequence of O st len F = k + 1 holds

Product (F,A1) = (Product (F,A2)) | E1

hence
SProduct (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;

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;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

Product (F,A2) in Funcs (E2,E2)
by FUNCT_2:9;(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;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

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

reconsider k = len F as Element of NAT ;

k = len F ;

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