let O, E1, E2 be set ; :: thesis:
let A1 be Action of O,E1; :: thesis:
let A2 be Action of O,E2; :: thesis:
let F be FinSequence of O; :: thesis:
assume A1: E1 c= E2 ; :: thesis:
assume A2: 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:
defpred S₁[ Element of NAT ] means for F being FinSequence of O st len F = $1 holds
Product F,A1 = (Product F,A2) | E1;
A3: S₁[ 0 ]

proof

let F be FinSequence of O; :: thesis:
assume A4: len F = 0 ; :: thesis:
E1 = E2 /\ E1 by A1, XBOOLE_1:28;
then dom (id E1) = E2 /\ E1 by RELAT_1:71;
then A5: dom (id E1) = (dom (id E2)) /\ E1 by RELAT_1:71;

A6: now

let x be set ; :: thesis:
assume A7: x in dom (id E1) ; :: thesis:
then A8: x in E1 ;
thus (id E1) . x = x by A7, FUNCT_1:35
.= (id E2) . x by A1, A8, FUNCT_1:35 ; :: thesis:

end;

thus Product F,A1 = id E1 by A4, Def3
.= (id E2) | E1 by A5, A6, FUNCT_1:68
.= (Product F,A2) | E1 by A4, Def3 ; :: thesis:

end;

per cases ;

suppose O is empty ; :: thesis:

then rng F = {} ;
then F = {} ;
then len F = 0 ;
hence Product F,A1 = (Product F,A2) | E1 by A3; :: thesis:

end;

suppose A9: not O is empty ; :: thesis:

A10: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A11: S₁[k] ; :: thesis:

now

let F be FinSequence of O; :: thesis:
assume A12: len F = k + 1 ; :: thesis:
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;
Product F,A1 in Funcs E1,E1 by FUNCT_2:12;
then consider f1 being Function such that
A15: ( Product F,A1 = f1 & dom f1 = E1 & rng f1 c= E1 ) by FUNCT_2:def 2;
Product F,A2 in Funcs E2,E2 by FUNCT_2:12;
then consider f2 being Function such that
A16: ( Product F,A2 = f2 & dom f2 = E2 & rng f2 c= E2 ) by FUNCT_2:def 2;
A17: dom ((Product F,A2) | E1) = E2 /\ E1 by A16, RELAT_1:90
.= E1 by A1, XBOOLE_1:28 ;

now

let x be set ; :: thesis:
assume A18: x in dom (Product F,A1) ; :: thesis:
then A19: x in E1 ;
A20: o in O by A9;
{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;
o in dom A1 by A20, FUNCT_2:def 1;
then A1 . o in rng A1 by FUNCT_1:12;
then consider f1 being Function such that
A21: ( f1 = A1 . o & dom f1 = E1 & rng f1 c= E1 ) by FUNCT_2:def 2;
o in dom A2 by A20, FUNCT_2:def 1;
then A2 . o in rng A2 by FUNCT_1:12;
then consider f2 being Function such that
A22: ( f2 = A2 . o & dom f2 = E2 & rng f2 c= E2 ) by FUNCT_2:def 2;
A23: Product Fo,A1 = f1 by A9, A21, Lm26;
A24: Product Fo,A2 = f2 by A9, A22, Lm26;
A25: Product F,A1 = (Product Fk,A1) * (Product Fo,A1) by A9, A13, Lm29
.= (Product Fk,A1) * f1 by A9, A21, Lm26 ;
A26: Product F,A2 = (Product Fk,A2) * (Product Fo,A2) by A9, A13, Lm29
.= (Product Fk,A2) * f2 by A9, A22, Lm26 ;
A27: f1 . x in rng f1 by A18, A21, FUNCT_1:12;
thus (Product F,A1) . x = (Product Fk,A1) . (f1 . x) by A18, A21, A25, FUNCT_1:23
.= ((Product Fk,A2) | E1) . (f1 . x) by A11, A14
.= (Product Fk,A2) . (f1 . x) by A21, A27, FUNCT_1:72
.= (Product Fk,A2) . ((f2 | E1) . x) by A2, A21, A22, A23, A24
.= (Product Fk,A2) . (f2 . x) by A18, FUNCT_1:72
.= ((Product Fk,A2) * f2) . x by A1, A19, A22, FUNCT_1:23
.= ((Product F,A2) | E1) . x by A18, A26, FUNCT_1:72 ; :: thesis:

end;

hence Product F,A1 = (Product F,A2) | E1 by A15, A17, FUNCT_1:9; :: thesis:

end;

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

end;

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

end;