let x, y be object ; :: thesis: for f being FinSequence st rng f = {x,y} & len f = 2 & not ( f . 1 = x & f . 2 = y ) holds
( f . 1 = y & f . 2 = x )
let f be FinSequence; :: thesis: ( rng f = {x,y} & len f = 2 & not ( f . 1 = x & f . 2 = y ) implies ( f . 1 = y & f . 2 = x ) )
assume that
A1: rng f = {x,y} and
A2: len f = 2 ; :: thesis: ( ( f . 1 = x & f . 2 = y ) or ( f . 1 = y & f . 2 = x ) )
2 in dom f by A2, Th25;
then A3: f . 2 in rng f by FUNCT_1:def 3;
A4: now :: thesis: ( f . 1 = y & f . 2 = y implies ( f . 1 = x & f . 2 = y ) )
x in rng f by A1, TARSKI:def 2;
then consider z being object such that
A5: z in dom f and
A6: x = f . z by FUNCT_1:def 3;
reconsider nz = z as Element of NAT by A5;
A7: ( 1 <= nz & nz <= len f ) by A5, Th25;
assume that
A8: f . 1 = y and
A9: f . 2 = y ; :: thesis: ( f . 1 = x & f . 2 = y )
per cases ( nz = 1 or nz = 1 + 1 ) by A2, A7, NAT_1:9;
suppose nz = 1 ; :: thesis: ( f . 1 = x & f . 2 = y )
hence ( f . 1 = x & f . 2 = y ) by A9, A6; :: thesis: verum
end;
suppose nz = 1 + 1 ; :: thesis: ( f . 1 = x & f . 2 = y )
hence ( f . 1 = x & f . 2 = y ) by A8, A9, A6; :: thesis: verum
end;
end;
end;
A10: now :: thesis: ( f . 1 = x & f . 2 = x implies ( f . 1 = x & f . 2 = y ) )
y in rng f by A1, TARSKI:def 2;
then consider z being object such that
A11: z in dom f and
A12: y = f . z by FUNCT_1:def 3;
reconsider nz = z as Element of NAT by A11;
A13: ( 1 <= nz & nz <= len f ) by A11, Th25;
assume that
A14: f . 1 = x and
A15: f . 2 = x ; :: thesis: ( f . 1 = x & f . 2 = y )
per cases ( nz = 1 or nz = 1 + 1 ) by A2, A13, NAT_1:9;
suppose nz = 1 ; :: thesis: ( f . 1 = x & f . 2 = y )
hence ( f . 1 = x & f . 2 = y ) by A14, A15, A12; :: thesis: verum
end;
suppose nz = 1 + 1 ; :: thesis: ( f . 1 = x & f . 2 = y )
hence ( f . 1 = x & f . 2 = y ) by A14, A12; :: thesis: verum
end;
end;
end;
1 in dom f by A2, Th25;
then f . 1 in rng f by FUNCT_1:def 3;
hence ( ( f . 1 = x & f . 2 = y ) or ( f . 1 = y & f . 2 = x ) ) by A1, A3, A10, A4, TARSKI:def 2; :: thesis: verum