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 . b1 misses G . b2 )
assume A3: x <> y ; :: thesis: G . b1 misses G . b2
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 . b1 misses G . b2
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 . b1 misses G . b2
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 y in dom F & y in dom G ) ; :: thesis: G . b1 misses G . b2
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;
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 . b1 misses F . b2 )
assume A9: x <> y ; :: thesis: F . b1 misses F . b2
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 . b1 misses F . b2
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 . b1 misses F . b2
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