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 S1[ Element of 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: S1[ 0 ]
proof
let F be FinSequence of O; :: thesis: ( len F = 0 implies Product F,A1 = (Product F,A2) | E1 )
A3: now
let x be set ; :: 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:35
.= (id E2) . x by A1, A5, FUNCT_1:35 ; :: thesis: verum
end;
E1 = E2 /\ E1 by A1, XBOOLE_1:28;
then dom (id E1) = E2 /\ E1 by RELAT_1:71;
then A6: dom (id E1) = (dom (id E2)) /\ E1 by RELAT_1:71;
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:68
.= (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 Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A11: S1[k] ; :: thesis: S1[k + 1]
now
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:22;
len F = (len Fk) + (len <*o*>) by A13, FINSEQ_1:35;
then A14: k + 1 = (len Fk) + 1 by A12, FINSEQ_1:56;
A15: now
{o} c= O by A9, ZFMISC_1:37;
then rng <*o*> c= O by FINSEQ_1:55;
then reconsider Fo = <*o*> as FinSequence of O by FINSEQ_1:def 4;
let x be set ; :: 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:12;
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, Lm26;
o in dom A2 by A18, FUNCT_2:def 1;
then A2 . o in rng A2 by FUNCT_1:12;
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, Lm26;
A26: f1 . x in rng f1 by A16, A20, FUNCT_1:12;
A27: Product F,A2 = (Product Fk,A2) * (Product Fo,A2) by A9, A13, Lm29
.= (Product Fk,A2) * f2 by A9, A23, Lm26 ;
Product F,A1 = (Product Fk,A1) * (Product Fo,A1) by A9, A13, Lm29
.= (Product Fk,A1) * f1 by A9, A19, Lm26 ;
hence (Product F,A1) . x = (Product Fk,A1) . (f1 . x) by A16, A20, FUNCT_1:23
.= ((Product Fk,A2) | E1) . (f1 . x) by A11, A14
.= (Product Fk,A2) . (f1 . x) by A21, A26, FUNCT_1:72
.= (Product Fk,A2) . ((f2 | E1) . x) by A8, A19, A23, A22, A25
.= (Product Fk,A2) . (f2 . x) by A16, FUNCT_1:72
.= ((Product Fk,A2) * f2) . x by A1, A17, A24, FUNCT_1:23
.= ((Product F,A2) | E1) . x by A16, A27, FUNCT_1:72 ;
:: thesis: verum
end;
Product F,A2 in Funcs E2,E2 by FUNCT_2:12;
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:90
.= E1 by A1, XBOOLE_1:28 ;
Product F,A1 in Funcs E1,E1 by FUNCT_2:12;
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:9; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A29: for k being Element of NAT holds S1[k] from NAT_1:sch 1(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;