let x be set ; :: thesis: for U1, U2 being non empty set
for p being FinSequence holds
( ( (U1 -multiCat) . x <> {} & (U2 -multiCat) . x <> {} implies (U1 -multiCat) . x = (U2 -multiCat) . x ) & ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) )
let U1, U2 be non empty set ; :: thesis: for p being FinSequence holds
( ( (U1 -multiCat) . x <> {} & (U2 -multiCat) . x <> {} implies (U1 -multiCat) . x = (U2 -multiCat) . x ) & ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) )
let p be FinSequence; :: thesis: ( ( (U1 -multiCat) . x <> {} & (U2 -multiCat) . x <> {} implies (U1 -multiCat) . x = (U2 -multiCat) . x ) & ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) )
reconsider e = {} as Element of {{}} by TARSKI:def 1;
defpred S₁[ Nat] means for U1, U2 being non empty set
for p being FinSequence st p is $1 + 1 -element holds
( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) );
A1: S₁[ 0 ]

proof

let U1, U2 be non empty set ; :: thesis: for p being FinSequence st p is 0 + 1 -element holds
( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) )
let p be FinSequence; :: thesis: ( p is 0 + 1 -element implies ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) ) )
set C1 = U1 -multiCat ;
set C2 = U2 -multiCat ;
A2: ( dom (U1 -multiCat) = (U1 *) * & dom (U2 -multiCat) = (U2 *) * ) by FUNCT_2:def 1;
{} /\ U1 = {} ;
then reconsider EE = {} as Subset of U1 ;
{} /\ U2 = {} ;
then reconsider EE2 = {} as Subset of U2 ;
reconsider E2 = EE2 * as non empty Subset of (U2 *) ;
reconsider eu2 = {} as Element of E2 by TARSKI:def 1;
reconsider E = EE * as non empty Subset of (U1 *) ;
reconsider euu = {} as Element of E by TARSKI:def 1;
assume p is 0 + 1 -element ; :: thesis: ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) )
then reconsider pp = p as 1 + 0 -element FinSequence ;
len pp = 1 by CARD_1:def 7;
then A3: p = {} ^ <*(p . 1)*> by FINSEQ_1:40
.= euu ^ <*(p . 1)*> ;

hereby :: thesis: ( ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) )

assume p is {} * -valued ; :: thesis: (U1 -multiCat) . p = {}
then p = euu ^ <*euu*> by A3;
hence (U1 -multiCat) . p = ((U1 -multiCat) . euu) ^ euu by Th33
.= {} ^ {}
.= {} ;
:: thesis: verum

end;

hereby :: thesis: ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p )

assume A4: ( (U1 -multiCat) . p = {} & p is U1 * -valued ) ; :: thesis: p is {{}} -valued
then reconsider ppp = pp as U1 * -valued non empty FinSequence ;
{(ppp . 1)} \ (U1 *) = {} ;
then reconsider l = pp . 1 as Element of U1 * by ZFMISC_1:60;
(U1 -multiCat) . p = ((U1 -multiCat) . euu) ^ l by Th33, A3
.= {} ^ l
.= l ;
then p = euu ^ <*euu*> by A3, A4;
hence p is {{}} -valued ; :: thesis: verum

end;

hereby :: thesis: verum

assume ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} ) ; :: thesis: (U1 -multiCat) . p = (U2 -multiCat) . p
then A5: ( p in (U1 *) * & p in (U2 *) * ) by FUNCT_1:def 2, A2;
reconsider p1 = pp as U1 * -valued non empty FinSequence by A5;
reconsider p2 = pp as U2 * -valued non empty FinSequence by A5;
A6: ( {(p1 . 1)} \ (U1 *) = {} & {(p2 . 1)} \ (U2 *) = {} ) ;
reconsider u1 = p1 . 1 as Element of U1 * by A6, ZFMISC_1:60;
reconsider u2 = p2 . 1 as Element of U2 * by A6, ZFMISC_1:60;
A7: (U1 -multiCat) . p = ((U1 -multiCat) . euu) ^ u1 by A3, Th33
.= {} ^ u1
.= u1 ;
(U2 -multiCat) . p = ((U2 -multiCat) . eu2) ^ u2 by A3, Th33
.= {} ^ u1
.= u1 ;
hence (U1 -multiCat) . p = (U2 -multiCat) . p by A7; :: thesis: verum

end;

end;

A8: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A9: S₁[n] ; :: thesis: S₁[n + 1]
let U1, U2 be non empty set ; :: thesis: for p being FinSequence st p is (n + 1) + 1 -element holds
( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) )
set C1 = U1 -multiCat ;
set C2 = U2 -multiCat ;
A10: ( dom (U1 -multiCat) = (U1 *) * & dom (U2 -multiCat) = (U2 *) * ) by FUNCT_2:def 1;
let p be FinSequence; :: thesis: ( p is (n + 1) + 1 -element implies ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) ) )
assume A11: p is (n + 1) + 1 -element ; :: thesis: ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) )
thus ( p is {} * -valued implies (U1 -multiCat) . p = {} ) :: thesis: ( ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) & ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p ) )

proof

{} /\ U1 = {} ;
then reconsider EE = {} as Subset of U1 ;
reconsider E = EE * as non empty Subset of (U1 *) ;
assume p is {} * -valued ; :: thesis: (U1 -multiCat) . p = {}
then reconsider pp = p as {} * -valued ((n + 1) + 1) + 0 -element FinSequence by A11;
reconsider p1 = pp | (Seg (n + 1)) as E -valued n + 1 -element FinSequence ;
{(pp . ((n + 1) + 1))} \ ({} *) = {} ;
then reconsider x1 = pp . ((n + 1) + 1) as Element of E by ZFMISC_1:60;
pp \+\ (p1 ^ <*x1*>) = {} ;
then ( pp = p1 ^ <*x1*> & p1 is U1 * -valued ) by Th29;
then (U1 -multiCat) . pp = ((U1 -multiCat) . p1) ^ x1 by Th33
.= ((U1 -multiCat) . p1) ^ {}
.= {} by A9 ;
hence (U1 -multiCat) . p = {} ; :: thesis: verum

end;

thus ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {{}} -valued ) :: thesis: ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} implies (U1 -multiCat) . p = (U2 -multiCat) . p )

proof

assume A12: ( (U1 -multiCat) . p = {} & p is U1 * -valued ) ; :: thesis: p is {{}} -valued
then reconsider pp = p as U1 * -valued ((n + 1) + 1) + 0 -element FinSequence by A11;
reconsider p1 = pp | (Seg (n + 1)) as U1 * -valued n + 1 -element FinSequence ;
{(pp . ((n + 1) + 1))} \ (U1 *) = {} ;
then reconsider x1 = pp . ((n + 1) + 1) as Element of U1 * by ZFMISC_1:60;
A13: pp \+\ (p1 ^ <*x1*>) = {} ;
then pp = p1 ^ <*x1*> by Th29;
then ((U1 -multiCat) . p1) ^ x1 = {} by Th33, A12;
then ( (U1 -multiCat) . p1 = {} & x1 = e ) ;
then ( (U1 -multiCat) . p1 = {} & <*x1*> = <*e*> ) ;
then reconsider p11 = p1, x11 = <*x1*> as {{}} -valued FinSequence by A9;
p11 ^ x11 is {{}} -valued ;
hence p is {{}} -valued by A13, Th29; :: thesis: verum

end;

assume A14: ( (U1 -multiCat) . p <> {} & (U2 -multiCat) . p <> {} ) ; :: thesis: (U1 -multiCat) . p = (U2 -multiCat) . p
then p in (U1 *) * by A10, FUNCT_1:def 2;
then reconsider p1 = p as U1 * -valued ((n + 1) + 1) + 0 -element FinSequence by A11;
reconsider q1 = p1 | (Seg (n + 1)) as U1 * -valued n + 1 -element FinSequence ;
{(p1 . ((n + 1) + 1))} \ (U1 *) = {} ;
then reconsider x1 = p1 . ((n + 1) + 1) as Element of U1 * by ZFMISC_1:60;
p in (U2 *) * by A14, A10, FUNCT_1:def 2;
then reconsider p2 = p as U2 * -valued ((n + 1) + 1) + 0 -element FinSequence by A11;
reconsider q2 = p2 | (Seg (n + 1)) as U2 * -valued n + 1 -element FinSequence ;
{(p2 . ((n + 1) + 1))} \ (U2 *) = {} ;
then reconsider x2 = p2 . ((n + 1) + 1) as Element of U2 * by ZFMISC_1:60;
( p1 \+\ (q1 ^ <*x1*>) = {} & p2 \+\ (q2 ^ <*x2*>) = {} ) ;
then ( p1 = q1 ^ <*x1*> & p2 = q2 ^ <*x2*> ) by Th29;
then A15: ( (U1 -multiCat) . p1 = ((U1 -multiCat) . q1) ^ x1 & (U2 -multiCat) . p2 = ((U2 -multiCat) . q2) ^ x2 ) by Th33;
assume A16: (U1 -multiCat) . p <> (U2 -multiCat) . p ; :: thesis: contradiction
then ( (U1 -multiCat) . q1 = {} or (U2 -multiCat) . q2 = {} ) by A9, A15;
then q1 is {{}} -valued by A9;
then ( (U1 -multiCat) . q1 = {} & (U2 -multiCat) . q2 = {} ) by A9;
hence contradiction by A16, A15; :: thesis: verum

end;

A17: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A8);
set C1 = U1 -multiCat ;
set C2 = U2 -multiCat ;
A18: ( dom (U1 -multiCat) = (U1 *) * & dom (U2 -multiCat) = (U2 *) * ) by FUNCT_2:def 1;

hereby :: thesis: ( ( p is {} * -valued implies (U1 -multiCat) . p = {} ) & ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued ) )

assume A19: ( (U1 -multiCat) . x <> {} & (U2 -multiCat) . x <> {} ) ; :: thesis: (U1 -multiCat) . x = (U2 -multiCat) . x
then ( x in (U1 *) * & x <> {} ) by A18, FUNCT_1:def 2;
then reconsider p = x as non empty FinSequence ;
consider m being Nat such that
A20: len p = m + 1 by NAT_1:6;
reconsider pp = p as m + 1 -element FinSequence by A20, CARD_1:def 7;
( (U1 -multiCat) . pp <> {} & (U2 -multiCat) . pp <> {} implies (U1 -multiCat) . pp = (U2 -multiCat) . pp ) by A17;
hence (U1 -multiCat) . x = (U2 -multiCat) . x by A19; :: thesis: verum

end;

hereby :: thesis: ( (U1 -multiCat) . p = {} & p is U1 * -valued implies p is {} * -valued )

assume A21: p is {} * -valued ; :: thesis: (U1 -multiCat) . p = {}

per cases ( p = {} or not p = {} ) ;

suppose p = {} ; :: thesis: (U1 -multiCat) . p = {}

hence (U1 -multiCat) . p = {} ; :: thesis: verum

end;

suppose not p = {} ; :: thesis: (U1 -multiCat) . p = {}

then consider m being Nat such that
A22: m + 1 = len p by NAT_1:6;
reconsider pp = p as m + 1 -element FinSequence by A22, CARD_1:def 7;
(U1 -multiCat) . pp = {} by A21, A17;
hence (U1 -multiCat) . p = {} ; :: thesis: verum

end;

end;

end;

assume A23: ( (U1 -multiCat) . p = {} & p is U1 * -valued ) ; :: thesis: p is {} * -valued

per cases ( p = {} or not p = {} ) ;

suppose p = {} ; :: thesis: p is {} * -valued

hence p is {} * -valued ; :: thesis: verum

end;

suppose not p = {} ; :: thesis: p is {} * -valued

then consider m being Nat such that
A24: m + 1 = len p by NAT_1:6;
reconsider pp = p as m + 1 -element FinSequence by A24, CARD_1:def 7;
pp is {} * -valued by A23, A17;
hence p is {} * -valued ; :: thesis: verum

end;

end;