let X be non empty set ; :: thesis: for F being FinSequence of X
for G being Function of NAT,X st ( for i being Nat holds F . i = G . i ) holds
( F is disjoint_valued iff G is disjoint_valued )
let F be FinSequence of X; :: thesis: for G being Function of NAT,X st ( for i being Nat holds F . i = G . i ) holds
( F is disjoint_valued iff G is disjoint_valued )
let G be Function of NAT,X; :: thesis: ( ( for i being Nat holds F . i = G . i ) implies ( F is disjoint_valued iff G is disjoint_valued ) )
assume A1: for i being Nat holds F . i = G . i ; :: thesis: ( F is disjoint_valued iff G is disjoint_valued )

hereby :: thesis: ( G is disjoint_valued implies F is disjoint_valued )

assume A2: F is disjoint_valued ; :: thesis: G is disjoint_valued

now :: thesis: for x, y being object st x <> y holds
G . x misses G . y

let x, y be object ; :: thesis: ( x <> y implies G . b₁ misses G . b₂ )
assume A3: x <> y ; :: thesis: G . b₁ misses G . b₂

per cases ( ( x in dom F & y in dom F ) or ( not x in dom F & x in dom G ) or ( not x in dom F & not x in dom G ) or ( not y in dom F & y in dom G ) or ( not y in dom F & not y in dom G ) ) ;

suppose ( x in dom F & y in dom F ) ; :: thesis: G . b₁ misses G . b₂

then ( G . x = F . x & G . y = F . y ) by A1;
hence G . x misses G . y by A2, A3, PROB_2:def 2; :: thesis: verum

end;

suppose ( not x in dom F & x in dom G ) ; :: thesis: G . b₁ misses G . b₂

then ( F . x = {} & G . x = F . x ) by A1, FUNCT_1:def 2;
hence G . x misses G . y by XBOOLE_1:65; :: thesis: verum

end;

suppose ( not x in dom F & not x in dom G ) ; :: thesis: G . b₁ misses G . b₂

then G . x = {} by FUNCT_1:def 2;
hence G . x misses G . y by XBOOLE_1:65; :: thesis: verum

end;

suppose ( not y in dom F & y in dom G ) ; :: thesis: G . b₁ misses G . b₂

then ( F . y = {} & G . y = F . y ) by A1, FUNCT_1:def 2;
hence G . x misses G . y by XBOOLE_1:65; :: thesis: verum

end;

suppose ( not y in dom F & not y in dom G ) ; :: thesis: G . b₁ misses G . b₂

then G . y = {} by FUNCT_1:def 2;
hence G . x misses G . y by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

hence G is disjoint_valued by PROB_2:def 2; :: thesis: verum

end;

assume A8: G is disjoint_valued ; :: thesis: F is disjoint_valued

now :: thesis: for x, y being object st x <> y holds
F . x misses F . y

let x, y be object ; :: thesis: ( x <> y implies F . b₁ misses F . b₂ )
assume A9: x <> y ; :: thesis: F . b₁ misses F . b₂

per cases ( ( x in dom G & y in dom G ) or not x in dom G or not y in dom G ) ;

suppose ( x in dom G & y in dom G ) ; :: thesis: F . b₁ misses F . b₂

then ( F . x = G . x & F . y = G . y ) by A1;
hence F . x misses F . y by A8, A9, PROB_2:def 2; :: thesis: verum

end;

suppose A10: ( not x in dom G or not y in dom G ) ; :: thesis: F . b₁ misses F . b₂

dom F c= NAT ;
then dom F c= dom G by FUNCT_2:def 1;
then ( not x in dom F or not y in dom F ) by A10;
then ( F . x = {} or F . y = {} ) by FUNCT_1:def 2;
hence F . x misses F . y by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

hence F is disjoint_valued by PROB_2:def 2; :: thesis: verum