let X be set ; for P, Q being a_partition of X
for f being Function of P,Q st ( for a being set st a in P holds
a c= f . a ) holds
for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
let P, Q be a_partition of X; for f being Function of P,Q st ( for a being set st a in P holds
a c= f . a ) holds
for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
let f be Function of P,Q; ( ( for a being set st a in P holds
a c= f . a ) implies for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q ) )
assume A1:
for a being set st a in P holds
a c= f . a
; for p being FinSequence of P
for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
let p be FinSequence of P; for q being FinSequence of Q holds
( product p c= product q iff f * p = q )
let q be FinSequence of Q; ( product p c= product q iff f * p = q )
A2:
rng p c= P
;
then
dom f = P
by FUNCT_2:def 1;
then A3:
dom (f * p) = dom p
by A2, RELAT_1:27;
hereby ( f * p = q implies product p c= product q )
assume A4:
product p c= product q
;
f * p = qthen A5:
dom p = dom q
by Th1;
now for x being object st x in dom p holds
(f * p) . x = q . xlet x be
object ;
( x in dom p implies (f * p) . x = q . x )assume A6:
x in dom p
;
(f * p) . x = q . xthen A7:
p . x c= q . x
by A4, Th1;
A8:
p . x in rng p
by A6, FUNCT_1:def 3;
A9:
q . x in rng q
by A5, A6, FUNCT_1:def 3;
reconsider Y =
X as non
empty set by A8;
reconsider P9 =
P,
Q9 =
Q as
a_partition of
Y ;
reconsider a =
p . x as
Element of
P9 by A8;
set z = the
Element of
a;
A10:
a c= f . a
by A1;
A11:
the
Element of
a in a
;
f . a in Q9
by FUNCT_2:5;
then
q . x = f . a
by A7, A9, A10, A11, Lm3;
hence
(f * p) . x = q . x
by A6, FUNCT_1:13;
verum end; hence
f * p = q
by A3, A5;
verum
end;
assume A12:
f * p = q
; product p c= product q
hence
product p c= product q
by A3, A12, CARD_3:27; verum